environ
vocabularies HIDDEN, FINSET_1, CARD_1, XBOOLE_0, SUBSET_1, SETFAM_1, TARSKI, ZFMISC_1, FUNCT_1, RELAT_1, FUNCOP_1, CARD_FIL, PCOMPS_1, STRUCT_0, ORDERS_2, YELLOW_1, CONNSP_2, YELLOW_6, NAT_1, ARYTM_3, PARTFUN1, PRE_TOPC, FINTOPO2, RCOMP_1, RLVECT_3, CANTOR_1, FILTER_0, XXREAL_1, YELLOW19, CARDFIL2, FINTOPO7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, SETFAM_1, FINSET_1, CARD_1, RELSET_1, CARD_FIL, STRUCT_0, DOMAIN_1, NUMBERS, ORDERS_2, YELLOW_1, NAT_1, CANTOR_1, FUNCT_2, FUNCOP_1, PARTFUN1, FINTOPO2, PRE_TOPC, CONNSP_2, CARDFIL2;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, FUNCT_1, FUNCT_2, SETFAM_1, ZFMISC_1, RELAT_1, XBOOLE_0, XBOOLE_1, CARD_FIL, WAYBEL_7, FINTOPO2, PRE_TOPC, CONNSP_2, CANTOR_1, YELLOW_9, SUBSET_1, PRE_CIRC, CARDFIL2;
schemes FUNCT_2, NAT_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, CARD_1, STRUCT_0, MEMBERED, FUNCT_2, ZFMISC_1, FINTOPO2, PRE_TOPC;
constructors HIDDEN, FINTOPO2, CANTOR_1, NAT_LAT, NAT_1, BORSUK_1, CARDFIL2, XXREAL_2, SIMPLEX0;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE;
equalities FUNCOP_1, FINTOPO2;
expansions TARSKI, XBOOLE_0, SETFAM_1, FINTOPO2, FUNCT_2, PRE_TOPC, CARDFIL2;