environ
vocabularies HIDDEN, SUBSET_1, NUMBERS, XBOOLE_0, FUNCOP_1, FUNCT_2, RELAT_1, TARSKI, FINSEQ_1, CARD_3, FUNCT_1, ZFMISC_1, ORDINAL4, CARD_1, XBOOLEAN, MARGREL1, PARTFUN1, NAT_1, UNIALG_1, FINSEQ_2, UNIALG_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, FUNCT_1, RELAT_1, NAT_1, FUNCT_2, XBOOLEAN, CARD_3, FINSEQ_1, FINSEQ_2, FUNCOP_1, PARTFUN1;
definitions TARSKI, XBOOLE_0, XBOOLEAN, FINSEQ_1, CARD_3, FUNCT_1;
theorems TARSKI, ZFMISC_1, FINSEQ_1, FUNCT_2, FUNCOP_1, XBOOLE_1, XBOOLEAN, FUNCT_1, CARD_3, FINSEQ_3, RELAT_1, RELSET_1, PARTFUN1, ORDINAL1, FINSEQ_2;
schemes XBOOLE_0, FUNCT_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, XBOOLEAN, FINSEQ_1, FINSEQ_2, ORDINAL1, RELSET_1, PARTFUN1, FUNCOP_1, CARD_1, CARD_3, FUNCT_2;
constructors HIDDEN, FUNCOP_1, XCMPLX_0, FINSEQ_1, XBOOLEAN, RELSET_1, CARD_3, FINSEQ_2, NUMBERS;
requirements HIDDEN, SUBSET, BOOLE, ARITHM, NUMERALS;
equalities XBOOLEAN, FINSEQ_1, FUNCOP_1, ORDINAL1;
expansions TARSKI, XBOOLEAN, CARD_3, FUNCT_1;