let X be non empty almost_discrete TopSpace; :: thesis: for A being Subset of X holds
( A is discrete iff for a, b being Point of X st a in A & b in A & a <> b holds
Cl {a} misses Cl {b} )
let A be Subset of X; :: thesis: ( A is discrete iff for a, b being Point of X st a in A & b in A & a <> b holds
Cl {a} misses Cl {b} )
thus ( A is discrete implies for a, b being Point of X st a in A & b in A & a <> b holds
Cl {a} misses Cl {b} ) :: thesis: ( ( for a, b being Point of X st a in A & b in A & a <> b holds
Cl {a} misses Cl {b} ) implies A is discrete )

proof

assume A1: A is discrete ; :: thesis: for a, b being Point of X st a in A & b in A & a <> b holds
Cl {a} misses Cl {b}
let a, b be Point of X; :: thesis: ( a in A & b in A & a <> b implies Cl {a} misses Cl {b} )
assume that
A2: a in A and
A3: b in A ; :: thesis: ( not a <> b or Cl {a} misses Cl {b} )
A4: A /\ (Cl {b}) = {b} by A1, A3, Th36;
assume A5: a <> b ; :: thesis: Cl {a} misses Cl {b}
assume (Cl {a}) /\ (Cl {b}) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then A6: Cl {a} meets Cl {b} ;
A /\ (Cl {a}) = {a} by A1, A2, Th36;
then {a} = {b} by A4, A6, Th50;
hence contradiction by A5, ZFMISC_1:3; :: thesis: verum

end;

assume A7: for a, b being Point of X st a in A & b in A & a <> b holds
Cl {a} misses Cl {b} ; :: thesis: A is discrete

now :: thesis: for x being Point of X st x in A holds
not A /\ (Cl {x}) <> {x}

let x be Point of X; :: thesis: ( x in A implies not A /\ (Cl {x}) <> {x} )
assume A8: x in A ; :: thesis: not A /\ (Cl {x}) <> {x}
assume A9: A /\ (Cl {x}) <> {x} ; :: thesis: contradiction
A10: {x} c= Cl {x} by PRE_TOPC:18;
{x} c= A by A8, ZFMISC_1:31;
then (A /\ (Cl {x})) \ {x} <> {} by A10, A9, Lm3, XBOOLE_1:19;
then consider y being object such that
A11: y in (A /\ (Cl {x})) \ {x} by XBOOLE_0:def 1;
reconsider y = y as Point of X by A11;
not y in {x} by A11, XBOOLE_0:def 5;
then A12: y <> x by TARSKI:def 1;
A13: y in A /\ (Cl {x}) by A11, XBOOLE_0:def 5;
then y in A by XBOOLE_0:def 4;
then Cl {y} misses Cl {x} by A7, A8, A12;
then A14: (Cl {y}) /\ (Cl {x}) = {} ;
y in Cl {x} by A13, XBOOLE_0:def 4;
then Cl {y} = Cl {x} by Th49;
hence contradiction by A14, PRE_TOPC:18, XBOOLE_1:3; :: thesis: verum

end;

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