let X be non empty TopSpace; :: thesis: for X1 being non empty everywhere_dense SubSpace of X
for X2 being non empty everywhere_dense SubSpace of X1 holds X2 is everywhere_dense SubSpace of X
let X1 be non empty everywhere_dense SubSpace of X; :: thesis: for X2 being non empty everywhere_dense SubSpace of X1 holds X2 is everywhere_dense SubSpace of X
let X2 be non empty everywhere_dense SubSpace of X1; :: thesis: X2 is everywhere_dense SubSpace of X
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:1;

now :: thesis: for A being Subset of X st A = the carrier of X2 holds
A is everywhere_dense

let A be Subset of X; :: thesis: ( A = the carrier of X2 implies A is everywhere_dense )
assume A1: A = the carrier of X2 ; :: thesis: A is everywhere_dense
then reconsider B = A as Subset of X1 by BORSUK_1:1;
A2: C is everywhere_dense by Def2;
B is everywhere_dense by A1, Def2;
hence A is everywhere_dense by A2, TOPS_3:64; :: thesis: verum

end;

hence X2 is everywhere_dense SubSpace of X by Def2, TSEP_1:7; :: thesis: verum