let X be non empty TopSpace; :: thesis: 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 c= the carrier of X0 & A c= C & A = B & A is nowhere_dense holds
B is nowhere_dense
let X0 be non empty SubSpace of X; :: thesis: for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is nowhere_dense holds
B is nowhere_dense
let C, A be Subset of X; :: thesis: for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is nowhere_dense holds
B is nowhere_dense
let B be Subset of X0; :: thesis: ( C is open & C c= the carrier of X0 & A c= C & A = B & A is nowhere_dense implies B is nowhere_dense )
assume A1: C is open ; :: thesis: ( not C c= the carrier of X0 or not A c= C or not A = B or not A is nowhere_dense or B is nowhere_dense )
assume A2: C c= the carrier of X0 ; :: thesis: ( not A c= C or not A = B or not A is nowhere_dense or B is nowhere_dense )
assume that
A3: A c= C and
A4: A = B ; :: thesis: ( not A is nowhere_dense or B is nowhere_dense )
assume A5: A is nowhere_dense ; :: thesis: B is nowhere_dense
A6: now :: thesis: ( C <> {} implies B is nowhere_dense )
assume C <> {} ; :: thesis: B is nowhere_dense
then consider X1 being non empty strict SubSpace of X such that
A7: C = the carrier of X1 by TSEP_1:10;
reconsider E = B as Subset of X1 by A3, A4, A7;
( E is nowhere_dense & X1 is SubSpace of X0 ) by A1, A2, A4, A5, A7, Lm1, TSEP_1:4;
hence B is nowhere_dense by Th68; :: thesis: verum
end;
now :: thesis: ( C = {} implies B is nowhere_dense )
assume C = {} ; :: thesis: B is nowhere_dense
then B = {} X0 by A3, A4, XBOOLE_1:3;
hence B is nowhere_dense ; :: thesis: verum
end;
hence B is nowhere_dense by A6; :: thesis: verum