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