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, Th57;
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;
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 A5; :: thesis: A /\ (Cl {x}) = {a}
Cl {x} = Cl {a} by A2, A4, Th49;
hence A /\ (Cl {x}) = {a} by A6, A5, 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 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 :: thesis: for x being object st x in D holds
x in A
let x be object ; :: 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, Th36;
hence x in A by A10, A12, XBOOLE_1:26, ZFMISC_1:18; :: thesis: verum
end;
then D c= A by TARSKI:def 3;
hence A = D by A10; :: 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:18;
assume x in A ; :: thesis: A /\ (Cl {x}) = {x}
then A14: {x} c= A by ZFMISC_1:31;
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:18; :: thesis: verum
end;
then A is discrete by Th52;
hence A is maximal_discrete by A8; :: thesis: verum