environ
vocabularies HIDDEN, STRUCT_0, XBOOLE_0, ZFMISC_1, ORDERS_2, WAYBEL_9, PRE_TOPC, FINSET_1, SUBSET_1, RCOMP_1, TARSKI, NATTRA_1, CARD_5, RELAT_2, FUNCT_1, WAYBEL_0, RELAT_1, SEQM_3, XXREAL_0, YELLOW_2, YELLOW_1, CARD_FIL, ORDINAL2, WELLORD1, WAYBEL_1, FUNCT_2, REWRITE1, LATTICES, YELLOW_0, LATTICE3, TDLAT_3, RLVECT_3, SETFAM_1, YELLOW_8, TOPS_1, CONNSP_2, PRELAMB, CANTOR_1, WAYBEL_2, YELLOW13, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, TOPS_2, FUNCT_1, RELSET_1, BINOP_1, FUNCT_2, FINSET_1, SETFAM_1, DOMAIN_1, STRUCT_0, ORDERS_2, PRE_TOPC, TOPS_1, COMPTS_1, TDLAT_2, TDLAT_3, LATTICE3, CANTOR_1, CONNSP_2, BORSUK_1, YELLOW_0, WAYBEL_0, YELLOW_1, ORDERS_3, WAYBEL_1, YELLOW_2, YELLOW_3, WAYBEL_2, YELLOW_8, WAYBEL_9;
definitions TARSKI, LATTICE3, PRE_TOPC, TOPS_2, WAYBEL_0, WAYBEL_1, YELLOW_8, BORSUK_1, XBOOLE_0, COMPTS_1;
theorems TARSKI, PRE_TOPC, ORDERS_2, TOPS_1, WAYBEL_3, CONNSP_2, TDLAT_3, SETFAM_1, COMPTS_1, CANTOR_1, ZFMISC_1, YELLOW_0, YELLOW_2, YELLOW_3, YELLOW_8, WAYBEL_1, WAYBEL14, YELLOW_9, URYSOHN1, YELLOW_4, WAYBEL_0, RELAT_1, TDLAT_2, FUNCT_1, FUNCT_2, ORDERS_3, BORSUK_1, TEX_1, WAYBEL_2, XBOOLE_0, XBOOLE_1, SUBSET_1, TOPS_2;
schemes FINSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, LATTICE3, YELLOW_0, TDLAT_3, TEX_1, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_3, YELLOW_9, YELLOW11, YELLOW12, RELAT_1;
constructors HIDDEN, SETFAM_1, TOPS_1, BORSUK_1, URYSOHN1, LATTICE3, TDLAT_2, TDLAT_3, T_0TOPSP, CANTOR_1, ORDERS_3, WAYBEL_1, WAYBEL_9, YELLOW_8, COMPTS_1, TOPS_2, WAYBEL_2;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities STRUCT_0, SUBSET_1, BINOP_1;
expansions TARSKI, LATTICE3, PRE_TOPC, BORSUK_1, XBOOLE_0, COMPTS_1;
Lm1:
for T being non empty TopStruct
for A being Subset of T
for p being Point of T st p in Cl A holds
for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q
Lm2:
for T being non empty TopStruct
for A being Subset of T
for p being Point of T st ( for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q ) holds
ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q
Lm3:
for T being non empty TopStruct
for A being Subset of T
for p being Point of T st ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q holds
p in Cl A