environ
vocabularies HIDDEN, XBOOLE_0, SUBSET_1, SETFAM_1, FUNCT_1, FINSEQ_1, PBOOLE, RELAT_1, NAT_1, PARTFUN1, SUPINF_2, MESFUNC1, ZFMISC_1, CARD_1, FINSET_1, XCMPLX_0, FUNCT_7, FUNCOP_1, VALUED_0, BINOP_1, STRUCT_0, ORDINAL1, MSUALG_6;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, SETFAM_1, FINSET_1, ORDINAL1, CARD_1, RELAT_1, XCMPLX_0, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, NAT_1, FINSEQ_1, FUNCOP_1, ZFMISC_1, PBOOLE, FUNCT_7;
definitions SUBSET_1, ZFMISC_1;
theorems TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, CARD_1, XBOOLE_1;
schemes ;
registrations XBOOLE_0, FUNCT_1, FUNCT_2, ZFMISC_1, ORDINAL1, CARD_1, FINSET_1, RELSET_1;
constructors HIDDEN, PARTFUN1, PBOOLE, ZFMISC_1, FUNCT_7, SETFAM_1, RELSET_1, XCMPLX_0, DOMAIN_1;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities SUBSET_1;
expansions SUBSET_1, ZFMISC_1;
:: Moved from ALG_1, GROUP_6, PRE_TOPC, POLYNOM1