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