let X0 be SubSpace of X; :: thesis: ( not X0 is proper implies X0 is everywhere_dense )
assume A2: not X0 is proper ; :: thesis: X0 is everywhere_dense

now

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 not A is proper by A2, TEX_2:13;
then A = [#] X by SUBSET_1:def 7;
hence A is everywhere_dense by TOPS_3:31; :: thesis: verum

end;

hence X0 is everywhere_dense by Def2; :: thesis: verum