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 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 = 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 = 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 = 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 = 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 = 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 ( A c= C & 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;
A4: Int D = Int (Cl B) by A1, A2, Th57;
assume A is nowhere_dense ; :: thesis: B is nowhere_dense
then ( Int (Cl A) = {} & Int D c= Int (Cl A) ) by A3, Def3, TOPS_1:48;
then Int (Cl B) = {} by A4, XBOOLE_1:3;
hence B is nowhere_dense by Def3; :: thesis: verum