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