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

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