environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, EQREL_1, SUBSET_1, TARSKI, SETFAM_1, FUNCT_1, RELAT_1, ZFMISC_1, FINSEQ_1, XXREAL_0, ARYTM_3, CARD_1, ORDINAL4, PARTIT1, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, SETFAM_1, FINSEQ_1, FINSEQ_4, EQREL_1, XXREAL_0;
definitions TARSKI, RELAT_1;
theorems TARSKI, FUNCT_1, SETFAM_1, EQREL_1, ZFMISC_1, RELAT_1, NAT_1, FINSEQ_1, FINSEQ_2, FUNCT_2, SUBSET_1, RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0;
schemes EQREL_1, NAT_1, CLASSES1, DOMAIN_1, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELSET_1, PARTFUN1, MEMBERED, EQREL_1, NAT_1, XXREAL_0;
constructors HIDDEN, SETFAM_1, FUNCT_2, XXREAL_0, XREAL_0, NAT_1, MEMBERED, EQREL_1, FINSEQ_4, RELSET_1, DOMAIN_1, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities EQREL_1;
expansions TARSKI, RELAT_1;