consider A0 being Subset of X such that
A5:
A0 <> the carrier of X
and
A6:
( A0 is dense & A0 is open )
by TEX_1:34;
not A0 is empty
by A6, TOPS_3:17;
then consider X0 being non empty strict open dense SubSpace of X such that
A7:
A0 = the carrier of X0
by A6, Th23;
take
X0
; ( X0 is dense & X0 is open & X0 is proper & X0 is strict & not X0 is empty )
A0 is proper
by A5, SUBSET_1:def 6;
hence
( X0 is dense & X0 is open & X0 is proper & X0 is strict & not X0 is empty )
by A7, TEX_2:8; verum