let X be non empty TopSpace; :: thesis: for x, y being Point of X holds
( MaxADSet x misses MaxADSet y iff ( ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) )
let x, y be Point of X; :: thesis: ( MaxADSet x misses MaxADSet y iff ( ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) )
thus ( not MaxADSet x misses MaxADSet y or ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) :: thesis: ( ( ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) implies MaxADSet x misses MaxADSet y )

proof

assume A1: (MaxADSet x) /\ (MaxADSet y) = {} ; :: according to XBOOLE_0:def 7 :: thesis: ( ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) )
assume A2: for V being Subset of X st V is open & MaxADSet x c= V holds
V meets MaxADSet y ; :: thesis: ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W )
set W = (Cl {x}) ` ;
set V = (Cl {y}) ` ;

now

take W = (Cl {x}) ` ; :: thesis: ( W is open & W misses MaxADSet x & MaxADSet y c= W )
thus W is open ; :: thesis: ( W misses MaxADSet x & MaxADSet y c= W )
MaxADSet x c= Cl {x} by Th50;
hence W misses MaxADSet x by SUBSET_1:44; :: thesis: MaxADSet y c= W

now

assume not MaxADSet y c= W ; :: thesis: contradiction
then (MaxADSet y) \ W <> {} by XBOOLE_1:37;
then consider a being set such that
A3: a in (MaxADSet y) \ W by XBOOLE_0:def 1;
A4: a in MaxADSet y by A3, XBOOLE_0:def 5;
reconsider a = a as Point of X by A3;
MaxADSet a = MaxADSet y by A4, Th23;
then A5: Cl {a} = Cl {y} by Th51;
not a in W by A3, XBOOLE_0:def 5;
then a in Cl {x} by SUBSET_1:50;
then {a} c= Cl {x} by ZFMISC_1:37;
then A6: Cl {y} c= Cl {x} by A5, TOPS_1:31;
MaxADSet y c= Cl {y} by Th50;
then (Cl {y}) ` misses MaxADSet y by SUBSET_1:44;
then not MaxADSet x c= (Cl {y}) ` by A2;
then (MaxADSet x) \ ((Cl {y}) ` ) <> {} by XBOOLE_1:37;
then consider b being set such that
A7: b in (MaxADSet x) \ ((Cl {y}) ` ) by XBOOLE_0:def 1;
A8: b in MaxADSet x by A7, XBOOLE_0:def 5;
reconsider b = b as Point of X by A7;
MaxADSet b = MaxADSet x by A8, Th23;
then A9: Cl {b} = Cl {x} by Th51;
not b in (Cl {y}) ` by A7, XBOOLE_0:def 5;
then b in Cl {y} by SUBSET_1:50;
then {b} c= Cl {y} by ZFMISC_1:37;
then Cl {x} c= Cl {y} by A9, TOPS_1:31;
then Cl {x} = Cl {y} by A6, XBOOLE_0:def 10;
then ( MaxADSet x = MaxADSet y & {x} c= MaxADSet x ) by Th14, Th51;
hence contradiction by A1; :: thesis: verum

end;

hence MaxADSet y c= W ; :: thesis: verum

end;

hence ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ; :: thesis: verum

end;

assume A10: ( ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) ; :: thesis: MaxADSet x misses MaxADSet y
assume MaxADSet x meets MaxADSet y ; :: thesis: contradiction
then A11: MaxADSet x = MaxADSet y by Th24;

now

per cases ( ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) by A10;

suppose ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) ; :: thesis: contradiction

then consider V being Subset of X such that
V is open and
A12: MaxADSet x c= V and
A13: V misses MaxADSet y ;
V /\ (MaxADSet y) = {} by A13, XBOOLE_0:def 7;
hence contradiction by A11, A12, XBOOLE_1:28; :: thesis: verum

end;

suppose ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ; :: thesis: contradiction

then consider W being Subset of X such that
W is open and
A14: W misses MaxADSet x and
A15: MaxADSet y c= W ;
W /\ (MaxADSet x) = {} by A14, XBOOLE_0:def 7;
hence contradiction by A11, A15, XBOOLE_1:28; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum