environ
vocabularies HIDDEN, PRE_TOPC, STRUCT_0, TARSKI, SUBSET_1, RCOMP_1, XBOOLE_0, ZFMISC_1, TDLAT_3, NATTRA_1, SETFAM_1, TSP_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, STRUCT_0, PRE_TOPC, BORSUK_1, TSEP_1, TDLAT_3, TEX_2, TEX_4;
definitions T_0TOPSP;
theorems ZFMISC_1, SUBSET_1, PRE_TOPC, TOPS_1, TSEP_1, TDLAT_3, TEX_1, TEX_2, TEX_4, TARSKI, STRUCT_0, XBOOLE_0, XBOOLE_1;
schemes ;
registrations XBOOLE_0, STRUCT_0, TOPS_1, TDLAT_3, TEX_1, TEX_2, SUBSET_1, ZFMISC_1;
constructors HIDDEN, REALSET2, BORSUK_1, TSEP_1, TDLAT_3, TEX_2, TEX_4, T_0TOPSP;
requirements HIDDEN, SUBSET, BOOLE;
equalities SUBSET_1, STRUCT_0;
expansions T_0TOPSP, SUBSET_1;
Lm1:
for X being non trivial anti-discrete TopStruct holds not X is T_0
Lm2:
for X being non empty TopSpace
for x being Point of X holds x in Cl {x}