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
for A being Subset of X st not A is empty holds
Cl A = the carrier of X by A1, TOPS_3:def 2;
hence X is anti-discrete by Th11; :: thesis: verum