let X be non empty TopSpace; :: thesis: for x, y being Point of X st MaxADSet x = MaxADSet y holds
Cl {x} = Cl {y}
let x, y be Point of X; :: thesis: ( MaxADSet x = MaxADSet y implies Cl {x} = Cl {y} )
assume A1: MaxADSet x = MaxADSet y ; :: thesis: Cl {x} = Cl {y}
then A2: y in MaxADSet x by Th21;
MaxADSet y is maximal_anti-discrete by Th20;
then A3: MaxADSet y is anti-discrete ;
x in MaxADSet y by A1, Th21;
hence Cl {x} = Cl {y} by A1, A2, A3; :: thesis: verum