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 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 dense
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 = [#] X by A1;
hence A is dense ; :: thesis: verum
end;
hence ( X0 is dense & X0 is strict & not X0 is empty ) ; :: thesis: verum