set X0 = the non empty strict non proper SubSpace of X;
take the non empty strict non proper SubSpace of X ; :: thesis: ( the non empty strict non proper SubSpace of X is strict & the non empty strict non proper SubSpace of X is T_0 )
thus ( the non empty strict non proper SubSpace of X is strict & the non empty strict non proper SubSpace of X is T_0 ) ; :: thesis: verum