let X be non empty TopSpace; :: thesis: for x, y being Point of X holds

( MaxADSet x = MaxADSet y iff Cl {x} = Cl {y} )

let x, y be Point of X; :: thesis: ( MaxADSet x = MaxADSet y iff Cl {x} = Cl {y} )

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: ( Cl {x} = Cl {y} implies MaxADSet x = MaxADSet y )

A2: MaxADSet y c= (MaxADSet x) \/ (MaxADSet y) by XBOOLE_1:7;

assume A3: Cl {x} = Cl {y} ; :: thesis: MaxADSet x = MaxADSet y

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: verum

( MaxADSet x = MaxADSet y iff Cl {x} = Cl {y} )

let x, y be Point of X; :: thesis: ( MaxADSet x = MaxADSet y iff Cl {x} = Cl {y} )

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: ( Cl {x} = Cl {y} implies MaxADSet x = MaxADSet y )

A2: MaxADSet y c= (MaxADSet x) \/ (MaxADSet y) by XBOOLE_1:7;

assume A3: Cl {x} = Cl {y} ; :: thesis: MaxADSet x = MaxADSet y

now :: thesis: for a being Point of X st a in (MaxADSet x) \/ (MaxADSet y) holds

(MaxADSet x) \/ (MaxADSet y) c= Cl {a}

then A9:
(MaxADSet x) \/ (MaxADSet y) is anti-discrete
;(MaxADSet x) \/ (MaxADSet y) c= Cl {a}

let a be Point of X; :: thesis: ( a in (MaxADSet x) \/ (MaxADSet y) implies (MaxADSet x) \/ (MaxADSet y) c= Cl {a} )

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

end;assume A4: a in (MaxADSet x) \/ (MaxADSet y) ; :: thesis: (MaxADSet x) \/ (MaxADSet y) c= Cl {a}

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

hence
(MaxADSet x) \/ (MaxADSet y) c= Cl {a}
; :: thesis: verumper cases
( a in MaxADSet x or a in MaxADSet y )
by A4, XBOOLE_0:def 3;

end;

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

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: verum

end;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: verum

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

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: verum

end;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: verum

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: verum