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 )

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

( 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

assume A10:
( ex V being Subset of X st
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 )

( W is open & W misses MaxADSet x & MaxADSet y c= W ) ; :: thesis: verum

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

hence
ex W being Subset 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

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

hence
MaxADSet y c= W
; :: thesis: verum
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;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

( W is open & W misses MaxADSet x & MaxADSet y c= W ) ; :: thesis: verum

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

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

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

suppose
ex V being Subset of X st

( V is open & MaxADSet x c= V & V misses MaxADSet y ) ; :: thesis: contradiction

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

suppose
ex W being Subset of X st

( W is open & W misses MaxADSet x & MaxADSet y c= W ) ; :: thesis: contradiction

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