environ
vocabularies HIDDEN, XBOOLE_0, ORDINAL1, FUNCT_1, SUBSET_1, RELAT_1, TARSKI, ZF_LANG, ZF_MODEL, BVFUNC_2, CARD_1, XBOOLEAN, FUNCT_4, ARYTM_3, ZF_COLLA;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, RELAT_1, FUNCT_1, ZF_LANG, ORDINAL1, NUMBERS, FUNCT_2, FUNCT_7, ZF_MODEL;
definitions TARSKI, ORDINAL1, XBOOLE_0;
theorems FUNCT_1, ZF_LANG, ZF_MODEL, ORDINAL1, ZFMISC_1, RELAT_1, XBOOLE_0, FUNCT_7, XREGULAR;
schemes TARSKI, CLASSES1, ORDINAL1, XBOOLE_0;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, MEMBERED, ZF_LANG, RELSET_1;
constructors HIDDEN, NAT_1, MEMBERED, ZF_MODEL, FUNCT_7, NUMBERS;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities ;
expansions TARSKI, XBOOLE_0;