let X be TopSpace; :: thesis: ( X is anti-discrete iff for A being Subset of X holds
( not A is open or A = {} or A = the carrier of X ) )
thus ( X is anti-discrete implies for A being Subset of X holds
( not A is open or A = {} or A = the carrier of X ) ) :: thesis: ( ( for A being Subset of X holds
( not A is open or A = {} or A = the carrier of X ) ) implies X is anti-discrete )

proof

assume A1: X is anti-discrete ; :: thesis: for A being Subset of X holds
( not A is open or A = {} or A = the carrier of X )
let A be Subset of X; :: thesis: ( not A is open or A = {} or A = the carrier of X )
assume A is open ; :: thesis: ( A = {} or A = the carrier of X )
then A in the topology of X by PRE_TOPC:def 5;
then A in {{} ,the carrier of X} by A1, Def2;
hence ( A = {} or A = the carrier of X ) by TARSKI:def 2; :: thesis: verum

end;

assume A2: for A being Subset of X holds
( not A is open or A = {} or A = the carrier of X ) ; :: thesis: X is anti-discrete
( {} in the topology of X & the carrier of X in the topology of X ) by PRE_TOPC:5, PRE_TOPC:def 1;
then A3: {{} ,the carrier of X} c= the topology of X by ZFMISC_1:38;

now

let P be set ; :: thesis: ( P in the topology of X implies P in {{} ,the carrier of X} )
assume A4: P in the topology of X ; :: thesis: P in {{} ,the carrier of X}
then reconsider C = P as Subset of X ;
C is open by A4, PRE_TOPC:def 5;
then ( C = {} or C = the carrier of X ) by A2;
hence P in {{} ,the carrier of X} by TARSKI:def 2; :: thesis: verum

end;

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