consider X0 being SubSpace of X;
take X0 ; :: thesis: X0 is anti-discrete
thus X0 is anti-discrete ; :: thesis: verum