environ
vocabularies HIDDEN, XBOOLE_0, SUBSET_1, ORDERS_2, SETFAM_1, WAYBEL_0, XXREAL_0, STRUCT_0, PRE_TOPC, FUNCT_1, RELAT_1, TARSKI, REWRITE1, ZFMISC_1, WAYBEL_9, RELAT_2, NATTRA_1, FINSET_1, LATTICES, FUNCOP_1, YELLOW_0, ORDINAL2, FUNCT_3, SEQM_3, CAT_1, WELLORD1, ARYTM_0, RLVECT_3, CANTOR_1, FUNCT_2, RCOMP_1, CONNSP_2, TOPS_1, LATTICE3, BORSUK_1, PRELAMB, CARD_FIL, PROB_1, YELLOW_6, WAYBEL11, YELLOW_9, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, FINSET_1, MCART_1, RELAT_2, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, STRUCT_0, WELLORD1, ORDERS_2, LATTICE3, ORDERS_3, YELLOW_0, WAYBEL_0, TDLAT_3, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_2, YELLOW_6, YELLOW_7, WAYBEL_9, WAYBEL11, CANTOR_1, BORSUK_1;
definitions TARSKI, STRUCT_0, PRE_TOPC, CANTOR_1, ORDERS_2, WAYBEL_0, WAYBEL_1, TOPS_2, WAYBEL11, XBOOLE_0;
theorems STRUCT_0, SETFAM_1, ENUMSET1, PRE_TOPC, CANTOR_1, YELLOW_0, WAYBEL_0, FUNCT_1, RELAT_1, FUNCT_2, TEX_1, ORDERS_2, ZFMISC_1, TARSKI, FINSET_1, FUNCOP_1, TDLAT_3, BORSUK_1, YELLOW_6, YELLOW_8, TOPS_1, CONNSP_2, WAYBEL_9, WAYBEL11, TOPS_2, LATTICE3, ORDERS_1, XBOOLE_0, XBOOLE_1, SUBSET_1;
schemes FRAENKEL, FUNCT_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FINSET_1, STRUCT_0, BORSUK_1, LATTICE3, YELLOW_0, TDLAT_3, TEX_1, WAYBEL_0, YELLOW_2, YELLOW_6, WAYBEL_9, WAYBEL11, FUNCT_2, CANTOR_1, RELSET_1;
constructors HIDDEN, SETFAM_1, TOLER_1, TOPS_1, TOPS_2, BORSUK_1, LATTICE3, TDLAT_3, CANTOR_1, ORDERS_3, WAYBEL11, RELSET_1;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities STRUCT_0, YELLOW_0, WAYBEL_0, WAYBEL11, WELLORD1;
expansions TARSKI, STRUCT_0, PRE_TOPC, ORDERS_2, WAYBEL_0, XBOOLE_0;
Lm1:
for S being TopStruct ex T being strict TopSpace st
( the carrier of T = the carrier of S & the topology of S is prebasis of T )