let X be non empty TopSpace; :: thesis:
let x, y be Point of X; :: thesis:
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:

proof

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

now :: thesis:

take W = (Cl {x}) ` ; :: thesis:
thus W is open ; :: thesis:
MaxADSet x c= Cl {x} by Th48;
hence W misses MaxADSet x by SUBSET_1:24; :: thesis:

now :: thesis:

MaxADSet y c= Cl {y} by Th48;
then (Cl {y}) ` misses MaxADSet y by SUBSET_1:24;
then not MaxADSet x c= (Cl {y}) ` by A2;
then (MaxADSet x) \ ((Cl {y}) `) <> {} by XBOOLE_1:37;
then consider b being object such that
A3: b in (MaxADSet x) \ ((Cl {y}) `) by XBOOLE_0:def 1;
A4: b in MaxADSet x by A3, XBOOLE_0:def 5;
reconsider b = b as Point of X by A3;
not b in (Cl {y}) ` by A3, XBOOLE_0:def 5;
then b in Cl {y} by SUBSET_1:29;
then A5: {b} c= Cl {y} by ZFMISC_1:31;
MaxADSet b = MaxADSet x by A4, Th21;
then Cl {b} = Cl {x} by Th49;
then A6: Cl {x} c= Cl {y} by A5, TOPS_1:5;
assume not MaxADSet y c= W ; :: thesis:
then (MaxADSet y) \ W <> {} by XBOOLE_1:37;
then consider a being object such that
A7: a in (MaxADSet y) \ W by XBOOLE_0:def 1;
A8: a in MaxADSet y by A7, XBOOLE_0:def 5;
reconsider a = a as Point of X by A7;
not a in W by A7, XBOOLE_0:def 5;
then a in Cl {x} by SUBSET_1:29;
then A9: {a} c= Cl {x} by ZFMISC_1:31;
MaxADSet a = MaxADSet y by A8, Th21;
then Cl {a} = Cl {y} by Th49;
then Cl {y} c= Cl {x} by A9, TOPS_1:5;
then Cl {x} = Cl {y} by A6;
then MaxADSet x = MaxADSet y by Th49;
hence contradiction by A1; :: thesis:

end;

hence MaxADSet y c= W ; :: thesis:

end;

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

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:
assume MaxADSet x meets MaxADSet y ; :: thesis:
then A11: MaxADSet x = MaxADSet y by Th22;

now :: thesis:

per cases by A10;

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

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;
hence contradiction by A11, A12, XBOOLE_1:28; :: thesis:

end;

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

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;
hence contradiction by A11, A15, XBOOLE_1:28; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis: