environ
vocabularies HIDDEN, WAYBEL_0, LATTICES, FUNCT_1, FINSET_1, SUBSET_1, STRUCT_0, FUNCOP_1, YELLOW_0, XBOOLE_0, RELAT_1, ORDINAL2, TARSKI, SEQM_3, XXREAL_0, LATTICE3, ORDERS_2, REWRITE1, CAT_1, FUNCT_3, EQREL_1, WELLORD1, WAYBEL_5, PRE_TOPC, ORDINAL1, CONNSP_2, TOPS_1, RCOMP_1, RELAT_2, WAYBEL_9, ARYTM_0, WAYBEL19, YELLOW_6, WAYBEL11, CANTOR_1, YELLOW_9, PROB_1, YELLOW_2, PRELAMB, WAYBEL21;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1, TOLER_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, CONNSP_2, COMPTS_1, CANTOR_1, ORDERS_2, LATTICE3, ORDERS_3, YELLOW_0, YELLOW_2, WAYBEL_0, WAYBEL_3, WAYBEL_5, YELLOW_6, YELLOW_7, WAYBEL_9, YELLOW_9, WAYBEL11, WAYBEL17, WAYBEL19;
definitions TARSKI, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, YELLOW_6, XBOOLE_0;
theorems YELLOW_0, WAYBEL_0, WAYBEL_6, PRE_TOPC, FUNCOP_1, RELAT_1, FUNCT_2, TOPS_1, TOPS_2, ZFMISC_1, CONNSP_2, WAYBEL_9, YELLOW_9, FUNCT_1, WAYBEL_1, YELLOW_6, WAYBEL19, SETWISEO, FUNCT_3, TARSKI, LATTICE3, WAYBEL11, WAYBEL17, ORDERS_2, YELLOW_2, WEIERSTR, COMPTS_1, WAYBEL10, YELLOW_7, YELLOW_4, WAYBEL20, RELSET_1, XBOOLE_0, XBOOLE_1;
schemes FRAENKEL, FINSET_1, LATTICE3, XBOOLE_0;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, STRUCT_0, PRE_TOPC, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_2, YELLOW_6, WAYBEL_9, WAYBEL10, WAYBEL17, YELLOW_9, WAYBEL19, SUBSET_1, TOPS_1, RELSET_1;
constructors HIDDEN, TOLER_1, TOPS_1, NATTRA_1, BORSUK_1, CANTOR_1, TOPS_2, ORDERS_3, YELLOW_2, WAYBEL_3, WAYBEL17, YELLOW_9, WAYBEL19, COMPTS_1, WAYBEL_2;
requirements HIDDEN, SUBSET, BOOLE;
equalities LATTICE3, YELLOW_0, WAYBEL_0, WELLORD1, RELAT_1, STRUCT_0;
expansions TARSKI, LATTICE3, YELLOW_0, WAYBEL_0, XBOOLE_0;