:: Numerals - Requirements :: by Library Committee :: :: Received February 27, 2003 :: Copyright (c) 2003-2021 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; 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 :: NUMERALS:1 {} is Element of omega; ::theorem :: numeral(X) implies X is Element of omega; ::theorem :: numeral(X) implies succ(X) = X + 1;