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 = the carrier of X0 & 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 = the carrier of X0 & 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 = the carrier of X0 & A = B & A is nowhere_dense holds
B is nowhere_dense
let B be Subset of X0; :: thesis: ( C is open & C = the carrier of X0 & A = B & A is nowhere_dense implies B is nowhere_dense )
assume A1: C is open ; :: thesis: ( not C = the carrier of X0 or not A = B or not A is nowhere_dense or B is nowhere_dense )
assume A2: C = the carrier of X0 ; :: thesis: ( not A = B or not A is nowhere_dense or B is nowhere_dense )
assume A = B ; :: thesis: ( not A is nowhere_dense or B is nowhere_dense )
then A3: Cl B c= Cl A by Th53;
then reconsider D = Cl B as Subset of X by XBOOLE_1:1;
assume A is nowhere_dense ; :: thesis: B is nowhere_dense
then A4: Int (Cl A) = {} ;
Int D = Int (Cl B) by A1, A2, Th57;
then Int (Cl B) = {} by A3, A4, TOPS_1:19, XBOOLE_1:3;
hence B is nowhere_dense ; :: thesis: verum