environ
vocabularies HIDDEN, CLASSES2, ZF_LANG, FUNCT_1, SUBSET_1, ZF_MODEL, TARSKI, ORDINAL1, XBOOLE_0, ZFMISC_1, CARD_1, BVFUNC_2, XBOOLEAN, ZFMODEL1, RELAT_1, ORDINAL2, ORDINAL4, CARD_3, CLASSES1, NUMBERS, NAT_1, ARYTM_3, XXREAL_0, REALSET1, FUNCT_2, ZF_REFLE, CARD_FIL, CARD_5;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, ZF_MODEL, ZFMODEL1, ORDINAL2, NUMBERS, CARD_3, CLASSES1, CLASSES2, ZF_LANG, ORDINAL4, ZF_LANG1, CARD_5, CARD_FIL, CARD_LAR, XXREAL_0;
definitions TARSKI, FUNCT_1, ZF_LANG, ZF_MODEL, WELLORD2, ORDINAL2, RELAT_1, XBOOLE_0, ORDINAL1;
theorems TARSKI, ZFMISC_1, NAT_1, FUNCT_1, FUNCT_2, ORDINAL1, ORDINAL2, ORDINAL3, ORDINAL4, CARD_1, CLASSES1, CLASSES2, ZF_LANG, ZF_MODEL, CARD_3, ZFMODEL1, FUNCT_5, ZF_LANG1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, FUNCT_7, CARD_LAR;
schemes CLASSES1, PARTFUN1, ORDINAL1, ORDINAL2, ZF_LANG, CARD_2, NAT_1;
registrations SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, ORDINAL2, XREAL_0, CARD_1, CLASSES2, ZF_LANG, ZF_LANG1, CLASSES1, ORDINAL4, CARD_5, CARD_LAR, CARD_3, RELAT_1;
constructors HIDDEN, ENUMSET1, WELLORD2, XXREAL_0, XREAL_0, NAT_1, CLASSES1, CARD_3, ORDINAL4, ZF_MODEL, ZFMODEL1, ZF_LANG1, RELSET_1, CARD_LAR, CARD_FIL, CARD_5, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET;
equalities ZF_LANG, ORDINAL2, XBOOLE_0, ORDINAL1;
expansions TARSKI, ORDINAL2, XBOOLE_0;