Reqmnts, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

### The abstract of the Mizar article:

### Numerals --- Requirements

**by****Library Committee**- Received February 27, 2003
- MML identifier: NUMERALS

- [ Mizar article, MML identifier index ]

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

Back to top