for X being non empty TopSpace
for X1 being everywhere_dense SubSpace of X
for X2 being SubSpace of X st X1 is SubSpace of X2 holds
X2 is everywhere_dense