environ
vocabularies HIDDEN, CARD_1, SUPINF_1, ARYTM_3, REAL_1, ARYTM_1, XBOOLE_0, SUBSET_1, NUMBERS, TARSKI, XXREAL_0, MEMBERED, ORDINAL2, XXREAL_2, FUNCT_1, RELAT_1, VALUED_0, CARD_3, FUNCT_4, FUNCOP_1, PARTFUN1, NAT_1, SERIES_1, SUPINF_2, MEMBER_1, MESFUNC1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, MEMBERED, XXREAL_0, XXREAL_3, XCMPLX_0, XREAL_0, REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, FUNCOP_1, VALUED_0, FUNCT_4, NAT_1, CARD_3, XXREAL_2, SUPINF_1, MEMBER_1;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, FUNCT_1, FUNCT_2, NAT_1, RELSET_1, CARD_4, FUNCT_4, FUNCOP_1, RELAT_1, ZFMISC_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, NUMBERS, XXREAL_2, XXREAL_3, CARD_3, MEMBER_1, MEMBERED, XREAL_0;
schemes FUNCT_2, RECDEF_1, NAT_1;
registrations RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSET_1, NUMBERS, XREAL_0, MEMBERED, VALUED_0, XXREAL_3, RELSET_1, MEMBER_1, NAT_1;
constructors HIDDEN, FUNCT_3, FUNCOP_1, FUNCT_4, FINSET_1, REAL_1, NAT_1, SUPINF_1, VALUED_1, XXREAL_2, XXREAL_3, CARD_3, RELSET_1, MEMBER_1, NUMBERS;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
equalities XBOOLE_0, XCMPLX_0, XXREAL_0, XXREAL_3, MEMBER_1;
expansions TARSKI, XBOOLE_0;
canceled;