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

now

let A be Subset of X; :: thesis: ( A = the carrier of X0 implies A is dense )
assume A = the carrier of X0 ; :: thesis: A is dense
then A is everywhere_dense by A1, Def2;
hence A is dense by TOPS_3:33; :: thesis: verum

end;

hence X0 is dense by Def1; :: thesis: verum