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