let X be non empty TopSpace; :: thesis: for x, y being Point of X holds
( MaxADSet x misses MaxADSet y iff Cl {x} <> Cl {y} )
let x, y be Point of X; :: thesis: ( MaxADSet x misses MaxADSet y iff Cl {x} <> Cl {y} )
thus ( MaxADSet x misses MaxADSet y implies Cl {x} <> Cl {y} ) by Th51; :: thesis: ( Cl {x} <> Cl {y} implies MaxADSet x misses MaxADSet y )
assume A1: Cl {x} <> Cl {y} ; :: thesis: MaxADSet x misses MaxADSet y
assume MaxADSet x meets MaxADSet y ; :: thesis: contradiction
then MaxADSet x = MaxADSet y by Th24;
hence contradiction by A1, Th51; :: thesis: verum