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 anti-discrete & not the non empty strict proper SubSpace of X is open & not the non empty strict proper SubSpace of X is closed & the non empty strict proper SubSpace of X is proper & the non empty strict proper SubSpace of X is strict )
thus ( the non empty strict proper SubSpace of X is anti-discrete & not the non empty strict proper SubSpace of X is open & not the non empty strict proper SubSpace of X is closed & the non empty strict proper SubSpace of X is proper & the non empty strict proper SubSpace of X is strict ) ; :: thesis: verum