environ
vocabularies HIDDEN, XBOOLE_0, PRE_TOPC, SUBSET_1, TSEP_2, STRUCT_0, TOPS_3, TOPS_1, ZFMISC_1, RCOMP_1, TARSKI, SETFAM_1, NATTRA_1, TDLAT_3;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1, TSEP_2, TDLAT_3, TOPS_3, TEX_2;
definitions TSEP_2;
theorems PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1, TMAP_1, TSEP_2, TOPS_3, TEX_1, TEX_2, XBOOLE_0, XBOOLE_1, SUBSET_1;
schemes ;
registrations XBOOLE_0, STRUCT_0, PRE_TOPC, BORSUK_1, TDLAT_3, TEX_1, TEX_2, TOPS_1;
constructors HIDDEN, TOPS_1, BORSUK_1, TSEP_1, TDLAT_3, TOPS_3, TEX_2, TSEP_2;
requirements HIDDEN, BOOLE, SUBSET;
equalities STRUCT_0;
expansions TSEP_2;
Lm1:
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense & B is everywhere_dense holds
A meets B
Lm2:
for X being non empty TopSpace
for A, B being Subset of X st ( ( A is everywhere_dense & B is dense ) or ( A is dense & B is everywhere_dense ) ) holds
A meets B