let X0 be non empty SubSpace of X; :: thesis: ( not X0 is proper implies not X0 is V144() )

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: X0 is V144()

then not A0 is proper by TEX_2:8;

then A0 = A ;

then not A0 is T_0 by Th4;

hence X0 is V144() ; :: thesis: verum

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: X0 is V144()

then not A0 is proper by TEX_2:8;

then A0 = A ;

then not A0 is T_0 by Th4;

hence X0 is V144() ; :: thesis: verum