let X0 be SubSpace of X; :: thesis: ( X0 is closed & X0 is maximal_T_0 implies not X0 is proper )
reconsider A = the carrier of X0 as Subset of X by Lm1;
assume X0 is closed ; :: thesis: ( not X0 is maximal_T_0 or not X0 is proper )
then A2: A is closed by TSEP_1:11;
assume X0 is maximal_T_0 ; :: thesis: not X0 is proper
then A is maximal_T_0 ;
then not A is proper by A2, Th3;
hence not X0 is proper by TEX_2:8; :: thesis: verum