let X1, X2 be TopSpace; :: thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D2 c= D1 & TopStruct(# the carrier of X1,the topology of X1 #) = TopStruct(# the carrier of X2,the topology of X2 #) & D1 is nowhere_dense holds
D2 is nowhere_dense
let D1 be Subset of X1; :: thesis: for D2 being Subset of X2 st D2 c= D1 & TopStruct(# the carrier of X1,the topology of X1 #) = TopStruct(# the carrier of X2,the topology of X2 #) & D1 is nowhere_dense holds
D2 is nowhere_dense
let D2 be Subset of X2; :: thesis: ( D2 c= D1 & TopStruct(# the carrier of X1,the topology of X1 #) = TopStruct(# the carrier of X2,the topology of X2 #) & D1 is nowhere_dense implies D2 is nowhere_dense )
assume A1: D2 c= D1 ; :: thesis: ( not TopStruct(# the carrier of X1,the topology of X1 #) = TopStruct(# the carrier of X2,the topology of X2 #) or not D1 is nowhere_dense or D2 is nowhere_dense )
assume A2: TopStruct(# the carrier of X1,the topology of X1 #) = TopStruct(# the carrier of X2,the topology of X2 #) ; :: thesis: ( not D1 is nowhere_dense or D2 is nowhere_dense )
assume D1 is nowhere_dense ; :: thesis: D2 is nowhere_dense
then ( Cl D1 is boundary & Cl D2 c= Cl D1 ) by A1, A2, Th81, TOPS_1:def 5;
then Cl D2 is boundary by A2, Th82;
hence D2 is nowhere_dense by TOPS_1:def 5; :: thesis: verum