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