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