let X be non empty TopSpace; :: thesis: ( ( for A being Subset of X st A <> the carrier of X holds
Int A = {} ) implies X is anti-discrete )
assume A1: for A being Subset of X st A <> the carrier of X holds
Int A = {} ; :: thesis: X is anti-discrete

now

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 = Int A by TOPS_1:55;
hence ( A = {} or A = the carrier of X ) by A1; :: thesis: verum

end;

hence X is anti-discrete by TDLAT_3:20; :: thesis: verum