environ
vocabularies HIDDEN, NUMBERS, FINSET_1, CARD_1, XBOOLE_0, ARYTM_3, ARYTM_1, SUBSET_1, XXREAL_0, NAT_1, RELAT_1, FINSEQ_1, ZFMISC_1, FUNCT_1, TARSKI, FUNCT_4, HALLMAR1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, FINSET_1, FINSEQ_1, FUNCT_2, FUNCT_7;
definitions TARSKI, XBOOLE_0;
theorems CARD_2, SPPOL_1, EULER_1, XBOOLE_1, ZFMISC_1, FUNCT_1, PARTFUN1, FINSET_1, PENCIL_1, CARD_1, TARSKI, NAT_1, XBOOLE_0, FINSEQ_1, FUNCT_7, FINSEQ_3, FINSEQ_5, TAXONOM1, RELAT_1, FUNCT_2, ENUMSET1, FINSEQ_2, XREAL_1, XXREAL_0, ORDINAL1;
schemes NAT_1, FUNCT_2, XBOOLE_0;
registrations SUBSET_1, RELAT_1, FUNCT_1, FINSET_1, XXREAL_0, XREAL_0, FINSEQ_1, CHAIN_1, ORDINAL1, CARD_1, RELSET_1;
constructors HIDDEN, REAL_1, NAT_1, FUNCT_7, RELSET_1, XREAL_0;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0, CARD_1, ORDINAL1;
expansions TARSKI, XBOOLE_0;