environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, STRUCT_0, PRE_TOPC, PENCIL_2, PENCIL_1, FUNCT_1, RELAT_1, TARSKI, SUBSET_1, PRALG_1, PBOOLE, ZFMISC_1, RELAT_2, FINSEQ_1, NAT_1, XXREAL_0, ARYTM_3, CARD_1, ARYTM_1, WAYBEL_3, RLVECT_2, CARD_3, INTEGRA1, FUNCT_4, FINSET_1, FDIFF_1, PARSP_1, GRAPH_2, FUNCT_2, CAT_1, RCOMP_1, FUNCOP_1, PENCIL_3, WAYBEL18;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XCMPLX_0, XXREAL_0, ORDINAL1, NUMBERS, NAT_1, RELAT_1, SUBSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, RELSET_1, CARD_1, FINSET_1, FINSEQ_1, CARD_3, DOMAIN_1, STRUCT_0, PRE_TOPC, PBOOLE, PZFMISC1, T_0TOPSP, PRALG_1, WAYBEL_3, PENCIL_1, FUNCT_7, PENCIL_2, TOPS_2, GRAPH_2;
definitions TARSKI, XBOOLE_0, PBOOLE, FUNCT_1, T_0TOPSP;
theorems XBOOLE_0, ZFMISC_1, FUNCT_1, FINSEQ_1, FINSEQ_3, NAT_1, CARD_3, PBOOLE, PRE_TOPC, FUNCT_7, PRALG_1, PZFMISC1, TARSKI, FUNCT_2, TOPS_2, PENCIL_1, PENCIL_2, CARD_1, XBOOLE_1, PUA2MSS1, FINSET_1, CARD_2, GRAPH_2, FUNCOP_1, RELAT_1, RELSET_1, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1;
schemes TRANSGEO, NAT_1, FINSEQ_2, PENCIL_2, FINSEQ_1, PBOOLE, CLASSES1;
registrations SUBSET_1, RELSET_1, FUNCT_2, XREAL_0, NAT_1, CARD_1, PBOOLE, STRUCT_0, PENCIL_1, ORDINAL1, FUNCT_1, RELAT_1, FINSEQ_1, PRE_POLY;
constructors HIDDEN, PZFMISC1, TOPS_2, REALSET2, T_0TOPSP, GRAPH_2, PENCIL_2, RELSET_1, PBOOLE, FUNCT_7, PRE_POLY;
requirements HIDDEN, REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
equalities XBOOLE_0, STRUCT_0, RELAT_1;
expansions TARSKI, XBOOLE_0, PBOOLE, FUNCT_1;