environ
vocabularies HIDDEN, XBOOLE_0, PBOOLE, SUBSET_1, NUMBERS, FINSEQ_1, STRUCT_0, MSUALG_1, RELAT_1, XXREAL_0, ARYTM_3, FUNCT_1, MSUALG_5, EQREL_1, TARSKI, LATTICES, XXREAL_2, REWRITE1, LATTICE3, SETFAM_1, ZFMISC_1, CARD_1, MSUALG_4, CLOSURE2, NAT_1, MARGREL1, PARTFUN1, FUNCT_4, FINSET_1, CARD_3, MSUALG_6, MSUALG_7, MSUALG_8;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, RELSET_1, DOMAIN_1, ORDINAL1, NUMBERS, XCMPLX_0, STRUCT_0, NAT_1, BINOP_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, FINSEQ_1, CARD_3, REWRITE1, EQREL_1, LATTICES, LATTICE3, PBOOLE, MSSUBFAM, MSUALG_1, MSUALG_4, MSUALG_5, CLOSURE2, MSUALG_6, MSUALG_7, XXREAL_0;
definitions TARSKI, XBOOLE_0;
theorems XBOOLE_0, TARSKI, PBOOLE, NAT_LAT, MSUALG_4, MSUALG_5, MSUALG_7, CLOSURE2, SETFAM_1, LATTICES, LATTICE3, MSSUBFAM, ZFMISC_1, FINSEQ_1, SUBSET_1, REWRITE1, RELAT_1, MSUALG_6, FUNCT_2, NAT_1, EQREL_1, VECTSP_8, CARD_3, XBOOLE_1, PARTFUN1;
schemes FINSEQ_1, PARTFUN1, CLASSES1;
registrations SUBSET_1, RELSET_1, PARTFUN1, FINSET_1, MEMBERED, EQREL_1, PBOOLE, STRUCT_0, LATTICES, MSUALG_1, MSUALG_3, MSUALG_5, CLOSURE2, MSUALG_6, MSUALG_7, FUNCT_1, XXREAL_0, XCMPLX_0, NAT_1;
constructors HIDDEN, BINOP_1, NAT_1, MEMBERED, REALSET1, REWRITE1, MSSUBFAM, LATTICE3, MSUALG_5, CLOSURE2, MSUALG_6, MSUALG_7, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0, EQREL_1;
expansions TARSKI, XBOOLE_0;