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 Th23;
MaxADSet y is maximal_anti-discrete by Th22;
then A3: MaxADSet y is anti-discrete by Def7;
x in MaxADSet y by A1, Th23;
hence Cl {x} = Cl {y} by A1, A2, A3, Def14; :: thesis: verum