let X1, X2 be non empty 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 everywhere_dense holds
D2 is everywhere_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 everywhere_dense holds
D2 is everywhere_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 everywhere_dense implies D2 is everywhere_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 everywhere_dense or D2 is everywhere_dense )
assume A2:
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
; ( not D1 is everywhere_dense or D2 is everywhere_dense )
assume
D1 is everywhere_dense
; D2 is everywhere_dense
then
Int D1 is dense
;
then
Int D2 is dense
by A1, A2, Th78, Th83;
hence
D2 is everywhere_dense
; verum