let X1, X2 be TopSpace; for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is dense holds
D2 is dense
let D1 be Subset of X1; for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is dense holds
D2 is dense
let D2 be Subset of X2; ( D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is dense implies D2 is dense )
assume A1:
D1 c= D2
; ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or not D1 is dense or D2 is dense )
then reconsider C2 = D1 as Subset of X2 by XBOOLE_1:1;
assume A2:
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
; ( not D1 is dense or D2 is dense )
assume
D1 is dense
; D2 is dense
then A3:
Cl D1 = the carrier of X1
;
Cl D1 = Cl C2
by A2, Th80;
then
C2 is dense
by A2, A3;
hence
D2 is dense
by A1, TOPS_1:44; verum