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

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

let A be Subset of X; :: thesis: ( A = the carrier of X0 implies A is open )
assume A = the carrier of X0 ; :: thesis: A is open
then A = [#] X by A1;
hence A is open ; :: thesis: verum

end;

hence ( X0 is dense & X0 is open & X0 is strict & not X0 is empty ) by TSEP_1:def 1; :: thesis: verum