### The Mizar article:

### Numerals --- Requirements

**by****Library Committee**

- Received February 27, 2003
Copyright (c) 2003 Association of Mizar Users

- MML identifier: NUMERALS
- [ MML identifier index ]

environ vocabulary ORDINAL2; notation SUBSET_1, ORDINAL2, NUMBERS; constructors ARYTM_3, XBOOLE_0, NUMBERS; clusters ZFMISC_1, XBOOLE_0; requirements BOOLE; theorems ORDINAL2, SUBSET_1; 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 :: "requirements SUBSET" needed 0 is Element of NAT by ORDINAL2:19,SUBSET_1:def 2; theorem 0 is natural by ORDINAL2:19,def 21; ::theorem :: numeral(X) implies :: X is natural Element of NAT;

Back to top