consider A0 being Subset of X such that
A7: A0 <> the carrier of X and
A8: ( A0 is dense & A0 is open ) by TEX_1:38;
not A0 is empty by A8, TOPS_3:17;
then consider X0 being non empty strict open dense SubSpace of X such that
A9: A0 = the carrier of X0 by A8, Th23;
take X0 ; :: thesis: ( X0 is dense & X0 is open & X0 is proper & X0 is strict & not X0 is empty )
A0 is proper by A7, SUBSET_1:def 7;
hence ( X0 is dense & X0 is open & X0 is proper & X0 is strict & not X0 is empty ) by A9, TEX_2:13; :: thesis: verum