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 )

( 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;

( 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 A8:
( ex E being Subset of X st
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 ) )

end;( 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
end;

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;

end;

( 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 ) )

( 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 ;

( 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;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 )

hence
( ex E being Subset 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;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

( 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

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 ) )

( 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 ;

( 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;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 )

hence
( ex E being Subset 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;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

( 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

( 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: contradictionend;

hence
contradiction
; :: thesis: verumper 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;

end;

( 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

( 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;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

suppose
ex F being Subset of X st

( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ; :: thesis: contradiction

( 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;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