let X be non empty almost_discrete TopSpace; :: thesis:
let A be Subset of X; :: thesis:
thus ( A is discrete implies for x being Point of X st x in Cl A holds
ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) ) :: thesis:

assume A1: A is discrete ; :: thesis:
let x be Point of X; :: thesis:
A2: Cl A = union { (Cl {a}) where a is Point of X : a in A } by Th48;
assume x in Cl A ; :: thesis:
then consider C being set such that
A3: x in C and
A4: C in { (Cl {a}) where a is Point of X : a in A } by A2, TARSKI:def 4;
consider a being Point of X such that
A5: C = Cl {a} and
A6: a in A by A4;

end;

hence ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) ; :: thesis:

end;

assume A7: for x being Point of X st x in Cl A holds
ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) ; :: thesis:
for x being Point of X st x in A holds
A /\ (Cl {x}) = {x}

end;