let X be non empty TopSpace; :: thesis: for X1 being non empty everywhere_dense SubSpace of X
for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1 is everywhere_dense SubSpace of X2
let X1 be non empty everywhere_dense SubSpace of X; :: thesis: for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1 is everywhere_dense SubSpace of X2
let X2 be non empty SubSpace of X; :: thesis: ( X1 is SubSpace of X2 implies X1 is everywhere_dense SubSpace of X2 )
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:35;
A1: C is everywhere_dense by Def2;
assume A2: X1 is SubSpace of X2 ; :: thesis: X1 is everywhere_dense SubSpace of X2
for A being Subset of X2 st A = the carrier of X1 holds
A is everywhere_dense by A1, TOPS_3:61;
hence X1 is everywhere_dense SubSpace of X2 by A2, Def2; :: thesis: verum