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

end;

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