let X be TopSpace; :: thesis: ( ( for A being Subset of X
for x being Point of X st A = {x} holds
Cl A = the carrier of X ) implies X is anti-discrete )
assume A1: for A being Subset of X
for x being Point of X st A = {x} holds
Cl A = the carrier of X ; :: thesis: X is anti-discrete
for B being Subset of X holds
( not B is closed or B = {} or B = the carrier of X )

proof

let B be Subset of X; :: thesis: ( not B is closed or B = {} or B = the carrier of X )
assume A2: B is closed ; :: thesis: ( B = {} or B = the carrier of X )
set z = the Element of B;
assume A3: B <> {} ; :: thesis: B = the carrier of X
then reconsider x = the Element of B as Point of X by TARSKI:def 3;
A4: {x} c= B by A3, ZFMISC_1:31;
then reconsider A = {x} as Subset of X by XBOOLE_1:1;
Cl A = the carrier of X by A1;
then the carrier of X c= B by A2, A4, TOPS_1:5;
hence B = the carrier of X ; :: thesis: verum

end;

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