set X0 = the SubSpace of X;
take the SubSpace of X ; :: thesis: the SubSpace of X is anti-discrete
thus the SubSpace of X is anti-discrete ; :: thesis: verum