let X0 be SubSpace of X; :: thesis: X0 is anti-discrete
A1: the topology of X = {{}, the carrier of X} by Def2;
now :: thesis: for S being object st S in the topology of X0 holds
S in {{}, the carrier of X0}
let S be object ; :: 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 4;
A5: ( B = the carrier of X implies A = the carrier of X0 ) by A4, BORSUK_1:1, 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} ;
now :: thesis: for S being object st S in {{}, the carrier of X0} holds
S in the topology of X0
let S be object ; :: 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:1, PRE_TOPC:def 1; :: thesis: verum
end;
then {{}, the carrier of X0} c= the topology of X0 ;
then the topology of X0 = {{}, the carrier of X0} by A6;
hence X0 is anti-discrete ; :: thesis: verum