consider X0 being non empty strict non proper SubSpace of X;
take X0 ; :: thesis: ( X0 is strict & not X0 is T_0 )
thus ( X0 is strict & not X0 is T_0 ) ; :: thesis: verum