environ
vocabularies HIDDEN, XBOOLE_0, SUBSET_1, ORDINAL1;
notations HIDDEN, XBOOLE_0, SUBSET_1, ORDINAL1;
definitions ;
theorems SUBSET_1, ORDINAL1;
schemes ;
registrations ;
constructors HIDDEN, SUBSET_1, ORDINAL1;
requirements HIDDEN, BOOLE;
equalities ;
expansions ;
:: "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.