let Y0 be non empty SubSpace of Y; :: thesis: ( Y0 is maximal_T_0 implies Y0 is T_0 )
assume A1: Y0 is maximal_T_0 ; :: thesis: Y0 is T_0
reconsider A = the carrier of Y0 as Subset of Y by Lm1;
A is maximal_T_0 by A1, Th11;
then A is T_0 by Def4;
hence Y0 is T_0 by TSP_1:15; :: thesis: verum