environ
vocabularies HIDDEN, PBOOLE, FUNCT_1, RELAT_1, TARSKI, FUNCT_4, FUNCOP_1, XBOOLE_0, SUBSET_1, FINSEQ_4, PARTFUN1, FUNCT_6, MEMBER_1, MSUALG_3, FINSET_1, ZFMISC_1, RELAT_2, MSAFREE2, BINOP_1, YELLOW_6, STRUCT_0, MSUALG_1, CLOSURE2, MSSUBFAM, SETFAM_1, CLOSURE1, SETLIM_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, SETFAM_1, RELAT_1, FUNCT_1, FINSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_4, PBOOLE, FUNCT_6, MSUALG_1, MSUALG_3, PRALG_1, MSSUBFAM;
definitions XBOOLE_0, FUNCT_1, MSSUBFAM, MSUALG_1, MSUALG_3, PBOOLE, FINSET_1, TARSKI;
theorems FUNCOP_1, FUNCT_1, FUNCT_2, FUNCT_4, MBOOLEAN, MSSUBFAM, MSUALG_3, PBOOLE, PZFMISC1, TARSKI, ZFMISC_1, PRALG_1, XBOOLE_0, PARTFUN1, RELAT_1;
schemes MSSUBFAM, PBOOLE, XBOOLE_0;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCOP_1, FINSET_1, PBOOLE, MSSUBFAM, MSUALG_1, RELAT_1, PRALG_1;
constructors HIDDEN, SETFAM_1, PZFMISC1, MSSUBFAM, PRALG_1, MSUALG_3, RELSET_1, FUNCT_4, FUNCT_6;
requirements HIDDEN, SUBSET, BOOLE;
equalities XBOOLE_0, FUNCOP_1;
expansions XBOOLE_0, FUNCT_1, MSUALG_1, PBOOLE, TARSKI;