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} )
then A2: A is discrete by Def7;
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
A3: x in C and
A4: 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
A5: C = Cl {a} and
A6: a in A by A4;

now

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, Th55;
hence A /\ (Cl {x}) = {a} by A2, A6, 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
thus A is maximal_discrete :: thesis: verum

proof

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}
consider a being Point of X such that
a in A and
A9: A /\ (Cl {x}) = {a} by A7;
( {x} c= A & {x} c= Cl {x} ) by A8, PRE_TOPC:48, ZFMISC_1:37;
hence A /\ (Cl {x}) = {x} by A9, XBOOLE_1:19, ZFMISC_1:24; :: thesis: verum

end;

then A10: A is discrete by Th58;
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 A11: D is discrete ; :: thesis: ( not A c= D or A = D )
assume A12: A c= D ; :: thesis: A = D
D c= A

proof

now

let x be set ; :: thesis: ( x in D implies x in A )
assume A13: x in D ; :: thesis: x in A
then reconsider y = x as Point of X ;
consider a being Point of X such that
A14: a in A and
A15: A /\ (Cl {y}) = {a} by A7;
D /\ (Cl {y}) = {y} by A11, A13, Th42;
hence x in A by A12, A14, A15, XBOOLE_1:26, ZFMISC_1:24; :: thesis: verum

end;

hence D c= A by TARSKI:def 3; :: thesis: verum

end;

hence A = D by A12, XBOOLE_0:def 10; :: thesis: verum

end;

hence A is maximal_discrete by A10, Def7; :: thesis: verum

end;