theorem Th16: :: TEX_3:16

for X being non empty TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is everywhere_dense iff A is everywhere_dense ) ;