let X be non empty TopSpace; :: thesis: for x, y being Point of X holds
( MaxADSet x = MaxADSet y iff Cl {x} = Cl {y} )
let x, y be Point of X; :: thesis: ( MaxADSet x = MaxADSet y iff Cl {x} = Cl {y} )
thus ( MaxADSet x = MaxADSet y implies Cl {x} = Cl {y} ) by Lm1; :: thesis: ( Cl {x} = Cl {y} implies MaxADSet x = MaxADSet y )
assume A1: Cl {x} = Cl {y} ; :: thesis: MaxADSet x = MaxADSet y
A2: (MaxADSet x) \/ (MaxADSet y) is anti-discrete

proof

now

let a be Point of X; :: thesis: ( a in (MaxADSet x) \/ (MaxADSet y) implies (MaxADSet x) \/ (MaxADSet y) c= Cl {a} )
assume A3: a in (MaxADSet x) \/ (MaxADSet y) ; :: thesis: (MaxADSet x) \/ (MaxADSet y) c= Cl {a}

now

per cases ( a in MaxADSet x or a in MaxADSet y ) by A3, XBOOLE_0:def 3;

suppose a in MaxADSet x ; :: thesis: (MaxADSet x) \/ (MaxADSet y) c= Cl {a}

then A4: MaxADSet a = MaxADSet x by Th23;
then A5: Cl {a} = Cl {x} by Lm1;
A6: MaxADSet x c= Cl {a} by A4, Th50;
MaxADSet y c= Cl {a} by A1, A5, Th50;
hence (MaxADSet x) \/ (MaxADSet y) c= Cl {a} by A6, XBOOLE_1:8; :: thesis: verum

end;

suppose a in MaxADSet y ; :: thesis: (MaxADSet x) \/ (MaxADSet y) c= Cl {a}

then A7: MaxADSet a = MaxADSet y by Th23;
then A8: Cl {a} = Cl {y} by Lm1;
A9: MaxADSet y c= Cl {a} by A7, Th50;
MaxADSet x c= Cl {a} by A1, A8, Th50;
hence (MaxADSet x) \/ (MaxADSet y) c= Cl {a} by A9, XBOOLE_1:8; :: thesis: verum

end;

end;

end;

hence (MaxADSet x) \/ (MaxADSet y) c= Cl {a} ; :: thesis: verum

end;

hence (MaxADSet x) \/ (MaxADSet y) is anti-discrete by Def12; :: thesis: verum

end;

A10: ( MaxADSet x is maximal_anti-discrete & MaxADSet y is maximal_anti-discrete ) by Th22;
( MaxADSet x c= (MaxADSet x) \/ (MaxADSet y) & MaxADSet y c= (MaxADSet x) \/ (MaxADSet y) ) by XBOOLE_1:7;
then ( MaxADSet x = (MaxADSet x) \/ (MaxADSet y) & MaxADSet y = (MaxADSet x) \/ (MaxADSet y) ) by A2, A10, Def7;
hence MaxADSet x = MaxADSet y ; :: thesis: verum