consider M being Subset of X such that
A1: M is maximal_T_0 by Th10;
not M is empty by A1, Th4;
then consider X0 being non empty strict SubSpace of X such that
A2: X0 is maximal_T_0 and
M = the carrier of X0 by A1, Th12;
take X0 ; :: thesis: ( X0 is maximal_T_0 & X0 is strict & not X0 is empty )
thus ( X0 is maximal_T_0 & X0 is strict & not X0 is empty ) by A2; :: thesis: verum