let X0 be SubSpace of X; :: thesis: ( X0 is dense & X0 is closed implies not X0 is proper )
assume A1: ( X0 is dense & X0 is closed ) ; :: thesis: not X0 is proper
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
( A is dense & A is closed ) by A1, Th9, TSEP_1:11;
then ( Cl A = the carrier of X & Cl A = A ) by PRE_TOPC:52, TOPS_3:def 2;
then not A is proper by SUBSET_1:def 7;
hence not X0 is proper by TEX_2:13; :: thesis: verum