environ
vocabularies HIDDEN, NUMBERS, FUNCT_1, CARD_3, RELAT_1, XBOOLE_0, TARSKI, CARD_1, ZFMISC_1, SUBSET_1, PRE_TOPC, STRUCT_0, RELAT_2, FINSEQ_1, NAT_1, XXREAL_0, ARYTM_3, FINSET_1, SETFAM_1, PRALG_1, PBOOLE, FUNCOP_1, WAYBEL_3, FUNCT_4, RLVECT_2, INTEGRA1, ARYTM_1, ORDINAL4, PENCIL_1, WAYBEL18;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, XCMPLX_0, SETFAM_1, CARD_1, ORDINAL1, NUMBERS, NAT_1, FINSET_1, RELAT_1, DOMAIN_1, STRUCT_0, FUNCT_1, PBOOLE, FUNCT_7, WAYBEL_3, FINSEQ_1, CARD_3, PRE_TOPC, PZFMISC1, FUNCOP_1, PRALG_1, XXREAL_0;
definitions TARSKI, WAYBEL_3, PBOOLE, XBOOLE_0, PRALG_1;
theorems TARSKI, FUNCT_1, FUNCOP_1, PBOOLE, CARD_3, PRALG_1, STRUCT_0, CARD_1, YELLOW11, ENUMSET1, FINSEQ_1, CARD_2, ZFMISC_1, NAT_1, FUNCT_7, YELLOW_6, PZFMISC1, PUA2MSS1, FINSEQ_3, RELAT_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1, SUBSET_1;
schemes FINSEQ_1, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, XREAL_0, CARD_3, PZFMISC1, STRUCT_0, YELLOW_6, ORDINAL1, CARD_1, ZFMISC_1, PRE_POLY, FUNCOP_1;
constructors HIDDEN, PZFMISC1, REALSET2, PRALG_1, WAYBEL_3, POLYNOM1, PBOOLE, FUNCT_7, FUNCT_4, RELSET_1, SETFAM_1;
requirements HIDDEN, REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
equalities STRUCT_0, CARD_1, ORDINAL1;
expansions TARSKI, WAYBEL_3, PBOOLE, XBOOLE_0;