X is SubSpace of X by TSEP_1:2;
then reconsider A0 = the carrier of X as Subset of X by TSEP_1:1;
consider X0 being non empty strict SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
take X0 ; :: thesis: ( X0 is everywhere_dense & X0 is strict & not X0 is empty )

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 = [#] X by A1;
hence A is everywhere_dense by TOPS_3:31; :: thesis: verum

end;

hence ( X0 is everywhere_dense & X0 is strict & not X0 is empty ) ; :: thesis: verum