let X0 be SubSpace of X; :: thesis: X0 is anti-discrete
A1: the topology of X = {{} ,the carrier of X} by Def2;

now

let S be set ; :: thesis: ( S in the topology of X0 implies S in {{} ,the carrier of X0} )
assume A2: S in the topology of X0 ; :: thesis: S in {{} ,the carrier of X0}
then reconsider A = S as Subset of X0 ;
consider B being Subset of X such that
A3: B in the topology of X and
A4: A = B /\ ([#] X0) by A2, PRE_TOPC:def 9;
A5: ( B = the carrier of X implies A = the carrier of X0 ) by A4, BORSUK_1:35, XBOOLE_1:28;
( B = {} implies A = {} ) by A4;
hence S in {{} ,the carrier of X0} by A1, A3, A5, TARSKI:def 2; :: thesis: verum

end;

then A6: the topology of X0 c= {{} ,the carrier of X0} by TARSKI:def 3;

now

let S be set ; :: thesis: ( S in {{} ,the carrier of X0} implies S in the topology of X0 )
assume S in {{} ,the carrier of X0} ; :: thesis: S in the topology of X0
then ( S = {} or S = the carrier of X0 ) by TARSKI:def 2;
hence S in the topology of X0 by PRE_TOPC:5, PRE_TOPC:def 1; :: thesis: verum

end;

then {{} ,the carrier of X0} c= the topology of X0 by TARSKI:def 3;
then the topology of X0 = {{} ,the carrier of X0} by A6, XBOOLE_0:def 10;
hence X0 is anti-discrete by Def2; :: thesis: verum