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) /\ () = {} ; :: 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:
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 () \ ((Cl {y}) `) by XBOOLE_0:def 1;
A4: b in MaxADSet x by ;
reconsider b = b as Point of X by A3;
not b in (Cl {y}) ` by ;
then b in Cl {y} by SUBSET_1:29;
then A5: {b} c= Cl {y} by ZFMISC_1:31;
then Cl {b} = Cl {x} by Th49;
then A6: Cl {x} c= Cl {y} by ;
then (MaxADSet y) \ W <> {} by XBOOLE_1:37;
then consider a being object such that
A7: a in () \ W by XBOOLE_0:def 1;
A8: a in MaxADSet y by ;
reconsider a = a as Point of X by A7;
not a in W by ;
then a in Cl {x} by SUBSET_1:29;
then A9: {a} c= Cl {x} by ZFMISC_1:31;
then Cl {a} = Cl {y} by Th49;
then Cl {y} c= Cl {x} by ;
then Cl {x} = Cl {y} by A6;
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:
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 /\ () = {} 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 /\ () = {} by A14;
hence contradiction by A11, A15, XBOOLE_1:28; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum