environ
vocabularies HIDDEN, CARD_1, FINSET_1, ORDINAL1, XBOOLE_0, TARSKI, CARD_3, CARD_5, ORDINAL2, SUBSET_1, RCOMP_1, XXREAL_2, SETFAM_1, FUNCT_1, NUMBERS, RELAT_1, ARYTM_3, CARD_FIL, CARD_2, CLASSES1, ZFMISC_1, CLASSES2, CARD_LAR, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, RELAT_1, CLASSES1, FUNCT_1, XCMPLX_0, NAT_1, SETFAM_1, FINSET_1, FUNCT_2, ORDINAL2, NUMBERS, CARD_2, CARD_3, CARD_5, CARD_FIL, CLASSES2;
definitions CLASSES1, ORDINAL1, TARSKI;
theorems TARSKI, FUNCT_1, FUNCT_2, ORDINAL1, ORDINAL2, ORDINAL3, CLASSES1, CLASSES2, CARD_3, CARD_1, CARD_2, CARD_4, CARD_5, SETFAM_1, ZFMISC_1, RELAT_1, SUBSET_1, CARD_FIL, XBOOLE_0, XBOOLE_1;
schemes DOMAIN_1, TREES_2, CARD_FIL, RECDEF_1, ORDINAL2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, ORDINAL3, CARD_1, CLASSES2, CARD_5, CARD_FIL, CARD_3, CLASSES1, CARD_2, NAT_1, XCMPLX_0;
constructors HIDDEN, WELLORD2, ORDINAL2, NAT_1, CARD_2, CLASSES1, CLASSES2, CARD_5, CARD_FIL, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE;
equalities ORDINAL1, SUBSET_1;
expansions TARSKI;
deffunc H1( Ordinal) -> set = Rank $1;
:: Some initial settings ::
:: ::