let X be non empty TopSpace; :: thesis: for x, y being Point of X holds
( MaxADSet x misses MaxADSet y iff ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) )

let x, y be Point of X; :: thesis: ( MaxADSet x misses MaxADSet y iff ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) )

thus ( not MaxADSet x misses MaxADSet y or ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) :: thesis: ( ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) implies MaxADSet x misses MaxADSet y )
proof
assume A1: MaxADSet x misses MaxADSet y ; :: thesis: ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) )

hereby :: thesis: verum
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 ;
suppose ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) ; :: thesis: ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) )

then consider V being Subset of X such that
A2: V is open and
A3: MaxADSet x c= V and
A4: V misses MaxADSet y ;
now :: thesis: ex F being Element of bool the carrier of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F )
take F = V ` ; :: thesis: ( F is closed & F misses MaxADSet x & MaxADSet y c= F )
thus F is closed by A2; :: thesis: ( F misses MaxADSet x & MaxADSet y c= F )
thus F misses MaxADSet x by ; :: thesis:
thus MaxADSet y c= F by ; :: thesis: verum
end;
hence ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) ; :: thesis: verum
end;
suppose ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ; :: thesis: ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) )

then consider W being Subset of X such that
A5: W is open and
A6: W misses MaxADSet x and
A7: MaxADSet y c= W ;
now :: thesis: ex E being Element of bool the carrier of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y )
take E = W ` ; :: thesis: ( E is closed & MaxADSet x c= E & E misses MaxADSet y )
thus E is closed by A5; :: thesis: ( MaxADSet x c= E & E misses MaxADSet y )
thus MaxADSet x c= E by ; :: thesis:
thus E misses MaxADSet y by ; :: thesis: verum
end;
hence ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) ; :: thesis: verum
end;
end;
end;
end;
assume A8: ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) ; :: thesis:
assume MaxADSet x meets MaxADSet y ; :: thesis: contradiction
then A9: MaxADSet x = MaxADSet y by Th22;
now :: thesis: contradiction
per cases ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) )
by A8;
suppose ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) ; :: thesis: contradiction
then consider E being Subset of X such that
E is closed and
A10: MaxADSet x c= E and
A11: E misses MaxADSet y ;
E /\ () = {} by A11;
hence contradiction by A9, A10, XBOOLE_1:28; :: thesis: verum
end;
suppose ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ; :: thesis: contradiction
then consider F being Subset of X such that
F is closed and
A12: F misses MaxADSet x and
A13: MaxADSet y c= F ;
F /\ () = {} by A12;
hence contradiction by A9, A13, XBOOLE_1:28; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum