let X be non empty TopSpace; :: thesis: ( ( for A being Subset of X holds Cl A = A ) implies X is discrete )
assume A1: for A being Subset of X holds Cl A = A ; :: thesis: X is discrete

now :: thesis: for A being Subset of X holds A is closed

let A be Subset of X; :: thesis: A is closed
Cl A = A by A1;
hence A is closed ; :: thesis: verum

end;

hence X is discrete by TDLAT_3:16; :: thesis: verum