theorem :: TEX_3:22

for X, 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 )