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

set V = (Cl {y}) ` ;
set W = (Cl {x}) ` ;
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 )

now :: thesis: ex W being Element of bool the carrier of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W )

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 Th48;
hence W misses MaxADSet x by SUBSET_1:24; :: thesis: MaxADSet y c= W

now :: thesis: MaxADSet y c= W

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: contradiction
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: 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 Th22;

now :: thesis: contradiction

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

end;

end;

end;

hence contradiction ; :: thesis: verum