environ
vocabularies HIDDEN, NUMBERS, FINSEQ_1, NAT_1, FINSEQ_3, RELAT_1, ARYTM_1, ORDINAL4, RFINSEQ, SUBSET_1, TARSKI, XBOOLE_0, XXREAL_0, ARYTM_3, CARD_1, FUNCT_1, PARTFUN1, PRALG_1, PBOOLE, RLVECT_2, FUNCT_4, STRUCT_0, PENCIL_1, CARD_3, INTEGRA1, ZFMISC_1, PRE_TOPC, FUNCT_2, CAT_1, RCOMP_1, RELAT_2, PENCIL_2, WAYBEL18;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, RELAT_1, NAT_D, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0, XXREAL_0, RFINSEQ, CARD_1, FINSEQ_1, CARD_3, PRE_TOPC, PBOOLE, PZFMISC1, TOPS_2, T_0TOPSP, PRALG_1, FUNCT_7, PENCIL_1;
definitions TARSKI, PBOOLE, PENCIL_1, XBOOLE_0;
theorems TARSKI, FUNCT_1, PBOOLE, CARD_3, CARD_1, FINSEQ_1, ZFMISC_1, NAT_1, FUNCT_7, YELLOW_6, PZFMISC1, PUA2MSS1, PRE_TOPC, FINSEQ_3, FUNCT_2, TOPGRP_1, TOPS_2, T_0TOPSP, RELAT_1, PENCIL_1, RFINSEQ, FINSEQ_4, FINSEQ_5, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, PARTFUN1, XREAL_0, NAT_D;
schemes FINSEQ_1, NAT_1, INT_1;
registrations SUBSET_1, FUNCT_1, PARTFUN1, FUNCT_2, XXREAL_0, XREAL_0, NAT_1, STRUCT_0, BORSUK_2, PENCIL_1, ORDINAL1, FINSEQ_1, RELSET_1, PRE_POLY;
constructors HIDDEN, RFINSEQ, NAT_D, PZFMISC1, TOPS_2, T_0TOPSP, POLYNOM1, PENCIL_1, REAL_1, RELSET_1, PBOOLE, FUNCT_7;
requirements HIDDEN, REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
equalities PENCIL_1, XBOOLE_0, STRUCT_0;
expansions TARSKI, PBOOLE, PENCIL_1, XBOOLE_0;