environ
vocabularies HIDDEN, NUMBERS, FINSEQ_1, ZFMISC_1, SUBSET_1, XXREAL_0, ARYTM_3, PARTFUN1, TARSKI, NAT_1, CARD_1, XBOOLE_0, FINSET_1, FUNCT_1, RELAT_1, ORDINAL1, COMPLEX1, ARYTM_1, STRUCT_0, ORDERS_2, EQREL_1, FUNCOP_1, FUNCT_2, RELAT_2, SETFAM_1, RCOMP_1, FIN_TOPO;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, FINSET_1, SETFAM_1, EQREL_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, DOMAIN_1, RELSET_1, FINSEQ_1, INT_2, NAT_1, XXREAL_0, STRUCT_0, ORDERS_2;
definitions TARSKI, STRUCT_0, ORDINAL1, XBOOLE_0, RELAT_2, ORDERS_2, SETFAM_1;
theorems NAT_1, TARSKI, FUNCOP_1, SUBSET_1, ZFMISC_1, FINSET_1, INT_1, CARD_1, FINSEQ_4, FUNCT_1, FUNCT_2, FINSEQ_1, ABSVALUE, RELSET_1, XBOOLE_0, XBOOLE_1, MEASURE2, XREAL_1, XXREAL_0, ORDINAL1, RELAT_1, EQREL_1, ORDERS_2, PARTFUN1;
schemes NAT_1, FINSEQ_2, DOMAIN_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCOP_1, XREAL_0, NAT_1, INT_1, STRUCT_0, FINSET_1;
constructors HIDDEN, DOMAIN_1, FUNCOP_1, REAL_1, INT_2, EQREL_1, FINSEQ_4, ORDERS_2, RELSET_1, XXREAL_0, MEASURE2, NAT_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities SUBSET_1, RELAT_1, FUNCOP_1;
expansions TARSKI, XBOOLE_0, ORDERS_2;