let X0 be non empty SubSpace of X; :: thesis: ( not X0 is proper implies not X0 is T_0 )
reconsider A0 = the carrier of X0 as non empty Subset of X by TSEP_1:1;
X is SubSpace of X by TSEP_1:2;
then reconsider A = the carrier of X as non empty Subset of X by TSEP_1:1;
assume not X0 is proper ; :: thesis: not X0 is T_0
then not A0 is proper by TEX_2:13;
then A0 = A by SUBSET_1:def 7;
then not A0 is T_0 by Th6;
hence not X0 is T_0 by Th15; :: thesis: verum