let X be non empty TopSpace; :: thesis: for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is everywhere_dense SubSpace of X iff Y2 is everywhere_dense SubSpace of X )
let X1, X2 be non empty TopSpace; :: thesis: ( X2 = TopStruct(# the carrier of X1, the topology of X1 #) implies ( X1 is everywhere_dense SubSpace of X iff X2 is everywhere_dense SubSpace of X ) )
assume A1: X2 = TopStruct(# the carrier of X1, the topology of X1 #) ; :: thesis: ( X1 is everywhere_dense SubSpace of X iff X2 is everywhere_dense SubSpace of X )
thus ( X1 is everywhere_dense SubSpace of X implies X2 is everywhere_dense SubSpace of X ) :: thesis: ( X2 is everywhere_dense SubSpace of X implies X1 is everywhere_dense SubSpace of X )
proof
assume A2: X1 is everywhere_dense SubSpace of X ; :: thesis: X2 is everywhere_dense SubSpace of X
then reconsider Y2 = X2 as SubSpace of X by A1, TMAP_1:7;
for A2 being Subset of X st A2 = the carrier of Y2 holds
A2 is everywhere_dense by A1, A2, Def2;
hence X2 is everywhere_dense SubSpace of X by Def2; :: thesis: verum
end;
assume A3: X2 is everywhere_dense SubSpace of X ; :: thesis: X1 is everywhere_dense SubSpace of X
then reconsider Y1 = X1 as SubSpace of X by A1, TMAP_1:7;
for A1 being Subset of X st A1 = the carrier of Y1 holds
A1 is everywhere_dense by A1, A3, Def2;
hence X1 is everywhere_dense SubSpace of X by Def2; :: thesis: verum