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;