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