set X0 = the strict proper SubSpace of X;
take the strict proper SubSpace of X ; :: thesis: ( the strict proper SubSpace of X is discrete & the strict proper SubSpace of X is open & the strict proper SubSpace of X is closed & the strict proper SubSpace of X is proper & the strict proper SubSpace of X is strict )
thus ( the strict proper SubSpace of X is discrete & the strict proper SubSpace of X is open & the strict proper SubSpace of X is closed & the strict proper SubSpace of X is proper & the strict proper SubSpace of X is strict ) ; :: thesis: verum