let X be non empty almost_discrete TopSpace; :: thesis: for A being Subset of X holds
( A is discrete iff 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} ) )
let A be Subset of X; :: thesis: ( A is discrete iff 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} ) )
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: ( ( 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} ) ) implies A is discrete )

proof

assume A1: A is discrete ; :: thesis: 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} )
let x be Point of X; :: thesis: ( x in Cl A implies ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) )
A2: Cl A = union { (Cl {a}) where a is Point of X : a in A } by Th48;
assume x in Cl A ; :: thesis: ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} )
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;

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

take a = a; :: thesis: ( a in A & A /\ (Cl {x}) = {a} )
thus a in A by A6; :: thesis: A /\ (Cl {x}) = {a}
Cl {x} = Cl {a} by A3, A5, Th49;
hence A /\ (Cl {x}) = {a} by A1, A6, Th36; :: thesis: verum

end;

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

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: A is discrete
for x being Point of X st x in A holds
A /\ (Cl {x}) = {x}

proof

let x be Point of X; :: thesis: ( x in A implies A /\ (Cl {x}) = {x} )
assume A8: x in A ; :: thesis: A /\ (Cl {x}) = {x}
A c= Cl A by PRE_TOPC:18;
then A9: ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) by A7, A8;
A10: {x} c= Cl {x} by PRE_TOPC:18;
{x} c= A by A8, ZFMISC_1:31;
hence A /\ (Cl {x}) = {x} by A9, A10, XBOOLE_1:19, ZFMISC_1:18; :: thesis: verum

end;

hence A is discrete by Th52; :: thesis: verum