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

now

let A be Subset of X; :: thesis: ( not A is empty implies Cl A = the carrier of X )
reconsider B = A as Subset of X ;
assume not A is empty ; :: thesis: Cl A = the carrier of X
then B is dense by A1;
hence Cl A = the carrier of X by TOPS_3:def 2; :: thesis: verum

end;

hence X is anti-discrete by Th13; :: thesis: verum