NUMERALS

:: Numerals - Requirements
::  by Library Committee
::
:: Received February 27, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, SUBSET_1, ORDINAL1;
 notations XBOOLE_0, SUBSET_1, ORDINAL1;
 constructors SUBSET_1, ORDINAL1;
 requirements BOOLE;
 theorems SUBSET_1, ORDINAL1;

begin

:: This file contains statements which are obvious for Mizar checker if
:: "requirements NUMERALS" is included in the environment description
:: of an article. They are published for testing purposes only.
:: Users should use appropriate requirements instead of referencing
:: to these theorems.
:: Some of these items need also other requirements for proper work.
:: Statements which cannot be expressed in Mizar language are commented out.

theorem
  {} is Element of omega
proof
  {} in omega by ORDINAL1:def 11;
  hence thesis by SUBSET_1:def 1;
end;
 
::theorem
::  numeral(X) implies X is Element of omega;
::theorem
::  numeral(X) implies succ(X) = X + 1;