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