environ
vocabularies HIDDEN, XBOOLE_0, STRUCT_0, PBOOLE, FUNCT_4, RELAT_1, CLOSURE2, SETFAM_1, MSUALG_1, TARSKI, MSUALG_2, UNIALG_2, MSSUBFAM, FUNCT_1, MARGREL1, SUBSET_1, FINSET_1, FUNCOP_1, WAYBEL_8, RELAT_2, MSAFREE2, BINOP_1, ZFMISC_1, CARD_3, FUNCT_2, CLOSURE3, PRE_POLY, SETLIM_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, STRUCT_0, PARTFUN1, FUNCT_2, FINSET_1, FUNCT_4, FUNCOP_1, PBOOLE, FINSEQ_2, MSUALG_1, MSUALG_2, CARD_3, PRE_POLY, CLOSURE2, MSSUBFAM, MBOOLEAN;
definitions TARSKI, XBOOLE_0, CLOSURE2, MSUALG_2, SETFAM_1, PBOOLE;
theorems FUNCT_4, FUNCT_1, TARSKI, PBOOLE, MSUALG_1, MBOOLEAN, FUNCOP_1, MSUALG_2, CLOSURE2, ZFMISC_1, RELAT_1, CARD_3, MSSUBFAM, FUNCT_2, XBOOLE_0, SETFAM_1, PARTFUN1, FINSET_1, PRE_POLY;
schemes CLASSES1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, PBOOLE, STRUCT_0, MSUALG_1, CLOSURE2, FINSEQ_1;
constructors HIDDEN, SETFAM_1, FUNCT_4, MSSUBFAM, MSUALG_2, PRALG_2, CLOSURE2, RELSET_1, FINSEQ_2, PRE_POLY;
requirements HIDDEN, SUBSET, BOOLE;
equalities PBOOLE, ORDINAL1;
expansions TARSKI, XBOOLE_0, CLOSURE2, MSUALG_2, SETFAM_1, PBOOLE;