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

proof

assume A1: A is maximal_discrete ; :: thesis: for x being Point of X ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} )
let x be Point of X; :: thesis: ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} )
the carrier of X = union { (Cl {a}) where a is Point of X : a in A } by A1, Th63;
then consider C being set such that
A2: x in C and
A3: C in { (Cl {a}) where a is Point of X : a in A } by TARSKI:def 4;
consider a being Point of X such that
A4: C = Cl {a} and
A5: a in A by A3;
A6: A is discrete by A1, Def7;

now

take a = a; :: thesis: ( a in A & A /\ (Cl {x}) = {a} )
thus a in A by A5; :: thesis: A /\ (Cl {x}) = {a}
Cl {x} = Cl {a} by A2, A4, Th55;
hence A /\ (Cl {x}) = {a} by A6, A5, Th42; :: 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 ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) ; :: thesis: A is maximal_discrete
A8: for D being Subset of X st D is discrete & A c= D holds
A = D

proof

let D be Subset of X; :: thesis: ( D is discrete & A c= D implies A = D )
assume A9: D is discrete ; :: thesis: ( not A c= D or A = D )
assume A10: A c= D ; :: thesis: A = D

now

let x be set ; :: thesis: ( x in D implies x in A )
assume A11: x in D ; :: thesis: x in A
then reconsider y = x as Point of X ;
A12: ex a being Point of X st
( a in A & A /\ (Cl {y}) = {a} ) by A7;
D /\ (Cl {y}) = {y} by A9, A11, Th42;
hence x in A by A10, A12, XBOOLE_1:26, ZFMISC_1:24; :: thesis: verum

end;

then D c= A by TARSKI:def 3;
hence A = D by A10, XBOOLE_0:def 10; :: thesis: verum

end;

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} )
A13: {x} c= Cl {x} by PRE_TOPC:48;
assume x in A ; :: thesis: A /\ (Cl {x}) = {x}
then A14: {x} c= A by ZFMISC_1:37;
ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) by A7;
hence A /\ (Cl {x}) = {x} by A14, A13, XBOOLE_1:19, ZFMISC_1:24; :: thesis: verum

end;

then A is discrete by Th58;
hence A is maximal_discrete by A8, Def7; :: thesis: verum