let X be non empty TopSpace; :: thesis:
let x, y be Point of X; :: thesis:
A1: MaxADSet x c= (MaxADSet x) \/ (MaxADSet y) by XBOOLE_1:7;
thus ( MaxADSet x = MaxADSet y implies Cl {x} = Cl {y} ) by Lm1; :: thesis:
A2: MaxADSet y c= (MaxADSet x) \/ (MaxADSet y) by XBOOLE_1:7;
assume A3: Cl {x} = Cl {y} ; :: thesis:

now :: thesis:

let a be Point of X; :: thesis:
assume A4: a in (MaxADSet x) \/ (MaxADSet y) ; :: thesis:

now :: thesis:

per cases by A4, XBOOLE_0:def 3;

suppose a in MaxADSet x ; :: thesis:

then A5: MaxADSet a = MaxADSet x by Th21;
then Cl {a} = Cl {x} by Lm1;
then A6: MaxADSet y c= Cl {a} by A3, Th48;
MaxADSet x c= Cl {a} by A5, Th48;
hence (MaxADSet x) \/ (MaxADSet y) c= Cl {a} by A6, XBOOLE_1:8; :: thesis:

end;

suppose a in MaxADSet y ; :: thesis:

then A7: MaxADSet a = MaxADSet y by Th21;
then Cl {a} = Cl {y} by Lm1;
then A8: MaxADSet x c= Cl {a} by A3, Th48;
MaxADSet y c= Cl {a} by A7, Th48;
hence (MaxADSet x) \/ (MaxADSet y) c= Cl {a} by A8, XBOOLE_1:8; :: thesis:

end;

end;

end;

hence (MaxADSet x) \/ (MaxADSet y) c= Cl {a} ; :: thesis:

end;

then A9: (MaxADSet x) \/ (MaxADSet y) is anti-discrete ;
A10: MaxADSet y is maximal_anti-discrete by Th20;
MaxADSet x is maximal_anti-discrete by Th20;
then MaxADSet x = (MaxADSet x) \/ (MaxADSet y) by A9, A1;
hence MaxADSet x = MaxADSet y by A9, A10, A2; :: thesis: