let X be non empty TopSpace; :: thesis: 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
let X1 be everywhere_dense SubSpace of X; :: thesis: for X2 being SubSpace of X st X1 is SubSpace of X2 holds
X2 is everywhere_dense
let X2 be SubSpace of X; :: thesis: ( X1 is SubSpace of X2 implies X2 is everywhere_dense )
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:1;
assume X1 is SubSpace of X2 ; :: thesis: X2 is everywhere_dense
then A1: the carrier of X1 c= the carrier of X2 by TSEP_1:4;
C is everywhere_dense by Def2;
then for A being Subset of X st A = the carrier of X2 holds
A is everywhere_dense by A1, TOPS_3:38;
hence X2 is everywhere_dense ; :: thesis: verum