environ
vocabularies HIDDEN, XBOOLE_0, WAYBEL_9, WAYBEL_0, SUBSET_1, CANTOR_1, WAYBEL11, STRUCT_0, REWRITE1, PRELAMB, YELLOW_9, PRE_TOPC, RELAT_2, ORDINAL2, CONNSP_2, ZFMISC_1, TARSKI, SETFAM_1, XXREAL_0, RLVECT_3, WAYBEL19, RCOMP_1, FINSET_1, YELLOW_2, RELAT_1, TOPS_1, LATTICE3, YELLOW_0, FUNCT_1, ORDERS_2, LATTICES, SEQM_3, YELLOW_6, CARD_FIL, EQREL_1, PROB_1, T_0TOPSP, ARYTM_3, WAYBEL_7, WAYBEL32, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FINSET_1, SETFAM_1, FUNCT_2, DOMAIN_1, STRUCT_0, ORDERS_2, LATTICE3, PRE_TOPC, TOPS_1, CONNSP_2, T_0TOPSP, YELLOW_0, WAYBEL_0, CANTOR_1, YELLOW_2, WAYBEL_2, YELLOW_6, WAYBEL_9, RELSET_1, WAYBEL11, WAYBEL19, YELLOW_9;
definitions TARSKI, WAYBEL_0, WAYBEL11, LATTICE3, WAYBEL_9, XBOOLE_0;
theorems YELLOW_9, CANTOR_1, PRE_TOPC, WAYBEL_0, CONNSP_2, WAYBEL11, ZFMISC_1, TARSKI, YELLOW_6, ORDERS_2, TOPS_2, TOPS_1, YELLOW_8, YELLOW_0, RELAT_1, FUNCT_1, YELLOW_2, SUBSET_1, FINSET_1, WAYBEL_2, SETFAM_1, TSP_1, WAYBEL21, WAYBEL_8, FUNCT_2, RELSET_1, XBOOLE_0, XBOOLE_1, STRUCT_0;
schemes FRAENKEL, DOMAIN_1, FUNCT_1, FUNCT_2;
registrations SUBSET_1, FUNCT_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_3, YELLOW_6, WAYBEL11, YELLOW_9, WAYBEL21, YELLOW14, WAYBEL29, TOPS_1, CARD_1, ORDINAL1, RELSET_1;
constructors HIDDEN, DOMAIN_1, TOPS_1, TOPS_2, CONNSP_2, LATTICE3, CANTOR_1, WAYBEL_1, WAYBEL11, YELLOW_9, RELSET_1, WAYBEL_2;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities WAYBEL_0, WAYBEL11, XBOOLE_0, SUBSET_1, STRUCT_0;
expansions TARSKI, WAYBEL_0, WAYBEL11, LATTICE3, WAYBEL_9, XBOOLE_0;