let X0 be non empty SubSpace of X; :: thesis: X0 is V138()
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;
A is T_0 by Th4;
then A0 is T_0 by Th5;
hence X0 is V138() by Th13; :: thesis: verum