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} )
A1: MaxADSet x c= () \/ () by XBOOLE_1:7;
thus ( MaxADSet x = MaxADSet y implies Cl {x} = Cl {y} ) by Lm1; :: thesis: ( Cl {x} = Cl {y} implies MaxADSet x = MaxADSet y )
A2: MaxADSet y c= () \/ () by XBOOLE_1:7;
assume A3: Cl {x} = Cl {y} ; :: thesis:
now :: thesis: for a being Point of X st a in () \/ () holds
() \/ () c= Cl {a}
let a be Point of X; :: thesis: ( a in () \/ () implies () \/ () c= Cl {a} )
assume A4: a in () \/ () ; :: thesis: () \/ () c= Cl {a}
now :: thesis: () \/ () c= Cl {a}end;
hence (MaxADSet x) \/ () c= Cl {a} ; :: thesis: verum
end;
then A9: (MaxADSet x) \/ () is anti-discrete ;
A10: MaxADSet y is maximal_anti-discrete by Th20;
MaxADSet x is maximal_anti-discrete by Th20;
then MaxADSet x = () \/ () by A9, A1;
hence MaxADSet x = MaxADSet y by A9, A10, A2; :: thesis: verum