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 A1, Th53;

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 A3, SUBSET_1:24; :: thesis: MaxADSet y c= F
thus MaxADSet y c= F by A4, SUBSET_1:23; :: 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 A6, SUBSET_1:23; :: thesis: E misses MaxADSet y
thus E misses MaxADSet y by A7, SUBSET_1:24; :: 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: MaxADSet x misses MaxADSet y
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 /\ (MaxADSet y) = {} 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 /\ (MaxADSet x) = {} by A12;
hence contradiction by A9, A13, XBOOLE_1:28; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum