environ
vocabularies HIDDEN, PRE_TOPC, SUBSET_1, XBOOLE_0, STRUCT_0, TOPS_1, TARSKI, RCOMP_1, TOPS_3;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1;
definitions PRE_TOPC, XBOOLE_0;
theorems PRE_TOPC, TOPS_1, TOPS_2, TSEP_1, TDLAT_3, SUBSET_1, TARSKI, XBOOLE_0, XBOOLE_1;
schemes ;
registrations PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1;
constructors HIDDEN, TOPS_1, BORSUK_1, TSEP_1;
requirements HIDDEN, BOOLE, SUBSET;
equalities XBOOLE_0, SUBSET_1, STRUCT_0;
expansions PRE_TOPC, XBOOLE_0;
Lm1:
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C = the carrier of X0 & A = B & A is nowhere_dense holds
B is nowhere_dense