let X0 be SubSpace of X; :: thesis: ( X0 is dense & X0 is open implies X0 is everywhere_dense )
assume A1: ( X0 is dense & X0 is open ) ; :: thesis: X0 is everywhere_dense

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

let A be Subset of X; :: thesis: ( A = the carrier of X0 implies A is everywhere_dense )
assume A = the carrier of X0 ; :: thesis: A is everywhere_dense
then ( A is dense & A is open ) by A1, TSEP_1:16;
hence A is everywhere_dense by TOPS_3:36; :: thesis: verum

end;

hence X0 is everywhere_dense ; :: thesis: verum