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