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;