let C be Simple_closed_curve; :: thesis: ( not LMP C in Lower_Arc C or not UMP C in Lower_Arc C )
assume A1: ( LMP C in Lower_Arc C & UMP C in Lower_Arc C ) ; :: thesis: contradiction
A2: ( UMP C in C & LMP C in C ) by Th43, Th44;
set n = |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|;
set s = |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|;
set S1 = LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C);
set S2 = LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|;
A3: UMP C <> W-min C by Th37;
A4: UMP C <> E-max C by Th38;
A5: LMP C <> W-min C by Th39;
A6: LMP C <> E-max C by Th40;
A7: LMP C <> UMP C by Th50;
A8: (Upper_Arc C) /\ (Lower_Arc C) = {(W-min C),(E-max C)} by JORDAN6:def 9;
A9: Upper_Arc C c= C by JORDAN6:76;
A10: Lower_Arc C c= C by JORDAN6:76;
A11: Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:def 8;
A12: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:def 9;
A13: now
assume UMP C in Upper_Arc C ; :: thesis: contradiction
then UMP C in (Upper_Arc C) /\ (Lower_Arc C) by A1, XBOOLE_0:def 4;
hence contradiction by A3, A4, A8, TARSKI:def 2; :: thesis: verum
end;
A14: now
assume LMP C in Upper_Arc C ; :: thesis: contradiction
then LMP C in (Upper_Arc C) /\ (Lower_Arc C) by A1, XBOOLE_0:def 4;
hence contradiction by A5, A6, A8, TARSKI:def 2; :: thesis: verum
end;
A15: (UMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;
A16: (LMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;
A17: |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;
A18: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;
A19: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 = S-bound C & |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 = N-bound C ) by EUCLID:56;
A20: (W-min C) `1 = W-bound C by EUCLID:56;
A21: (E-max C) `1 = E-bound C by EUCLID:56;
A22: LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C) is vertical by A15, A17, SPPOL_1:37;
A23: LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| is vertical by A16, A18, SPPOL_1:37;
A24: UMP C in LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C) by RLTOPSP1:69;
A25: LMP C in LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| by RLTOPSP1:69;
A26: W-bound C < E-bound C by SPRECT_1:33;
A27: LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C) misses LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| by Th55;
A28: for p being Point of (TOP-REAL 2) st p in Upper_Arc C holds
( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 & p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) by A9, A19, PSCOMP_1:71;
A29: for p being Point of (TOP-REAL 2) st p in Upper_Arc C holds
( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A9, A20, A21, PSCOMP_1:71;
A30: Upper_Arc C misses LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)
proof
assume Upper_Arc C meets LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C) ; :: thesis: contradiction
then consider x being set such that
A31: x in Upper_Arc C and
A32: x in LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C) by XBOOLE_0:3;
A33: (LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) /\ C = {(UMP C)} by Th47;
x in (LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) /\ C by A9, A31, A32, XBOOLE_0:def 4;
then A34: x = UMP C by A33, TARSKI:def 1;
then x in (Lower_Arc C) /\ (Upper_Arc C) by A1, A31, XBOOLE_0:def 4;
hence contradiction by A3, A4, A8, A34, TARSKI:def 2; :: thesis: verum
end;
A35: Upper_Arc C misses LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|
proof
assume Upper_Arc C meets LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| ; :: thesis: contradiction
then consider x being set such that
A36: x in Upper_Arc C and
A37: x in LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| by XBOOLE_0:3;
A38: (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) /\ C = {(LMP C)} by Th48;
x in (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) /\ C by A9, A36, A37, XBOOLE_0:def 4;
then A39: x = LMP C by A38, TARSKI:def 1;
then x in (Lower_Arc C) /\ (Upper_Arc C) by A1, A36, XBOOLE_0:def 4;
hence contradiction by A5, A6, A8, A39, TARSKI:def 2; :: thesis: verum
end;
per cases ( LE LMP C, UMP C,C or LE UMP C, LMP C,C ) by A2, JORDAN16:11;
suppose LE LMP C, UMP C,C ; :: thesis: contradiction
then A40: LE LMP C, UMP C, Lower_Arc C, E-max C, W-min C by A14, JORDAN6:def 10;
set S = Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C);
A41: UMP C in Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C) by A12, A40, JORDAN16:9;
A42: LMP C in Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C) by A12, A40, JORDAN16:9;
A43: Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C) c= Lower_Arc C by JORDAN16:5;
then A44: Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C) c= C by A10, XBOOLE_1:1;
A45: (LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) = {(UMP C)}
proof
(LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) /\ C = {(UMP C)} by Th47;
hence (LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) c= {(UMP C)} by A44, XBOOLE_1:26; :: according to XBOOLE_0:def 10 :: thesis: {(UMP C)} c= (LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(UMP C)} or x in (LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) )
assume x in {(UMP C)} ; :: thesis: x in (LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))
then A46: x = UMP C by TARSKI:def 1;
UMP C in LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C) by RLTOPSP1:69;
hence x in (LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) by A41, A46, XBOOLE_0:def 4; :: thesis: verum
end;
A47: (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) = {(LMP C)}
proof
(LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) /\ C = {(LMP C)} by Th48;
hence (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) c= {(LMP C)} by A44, XBOOLE_1:26; :: according to XBOOLE_0:def 10 :: thesis: {(LMP C)} c= (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(LMP C)} or x in (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) )
assume x in {(LMP C)} ; :: thesis: x in (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))
then x = LMP C by TARSKI:def 1;
hence x in (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) by A25, A42, XBOOLE_0:def 4; :: thesis: verum
end;
A48: ((LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) \/ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))) /\ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) = ((LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) /\ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) \/ ((Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) /\ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) by XBOOLE_1:23
.= {} \/ ((Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) /\ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) by A27, XBOOLE_0:def 7 ;
Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C) is_an_arc_of LMP C, UMP C by A7, A12, A40, JORDAN16:36;
then Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C) is_an_arc_of UMP C, LMP C by JORDAN5B:14;
then (LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) \/ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) is_an_arc_of |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|, LMP C by A45, TOPREAL1:17;
then ((LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) \/ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))) \/ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) is_an_arc_of |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| by A47, A48, TOPREAL1:16;
then A49: ((LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) \/ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))) \/ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) is_an_arc_of |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| by JORDAN5B:14;
A50: Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C) c= (Lower_Arc C) \ {(W-min C),(E-max C)}
proof
let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C) or s in (Lower_Arc C) \ {(W-min C),(E-max C)} )
assume A51: s in Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C) ; :: thesis: s in (Lower_Arc C) \ {(W-min C),(E-max C)}
now
assume s in {(W-min C),(E-max C)} ; :: thesis: contradiction
then ( s = W-min C or s = E-max C ) by TARSKI:def 2;
hence contradiction by A3, A6, A12, A51, Th11; :: thesis: verum
end;
hence s in (Lower_Arc C) \ {(W-min C),(E-max C)} by A43, A51, XBOOLE_0:def 5; :: thesis: verum
end;
Upper_Arc C misses Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)
proof
assume Upper_Arc C meets Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C) ; :: thesis: contradiction
then consider x being set such that
A52: x in Upper_Arc C and
A53: x in Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C) by XBOOLE_0:3;
x in Lower_Arc C by A50, A53, XBOOLE_0:def 5;
then x in (Lower_Arc C) /\ (Upper_Arc C) by A52, XBOOLE_0:def 4;
hence contradiction by A8, A50, A53, XBOOLE_0:def 5; :: thesis: verum
end;
then A54: Upper_Arc C misses ((LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) \/ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))) \/ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) by A30, A35, Lm4;
A55: now
let p be Point of (TOP-REAL 2); :: thesis: ( p in ((LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) \/ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))) \/ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) implies ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) )
assume A56: p in ((LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) \/ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))) \/ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ; :: thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
per cases ( p in LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C) or p in Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C) or p in LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| ) by A56, Lm3;
suppose A57: p in LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C) ; :: thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
A58: (UMP C) `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by A19, Th52;
then ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= (UMP C) `2 & (UMP C) `2 <= p `2 ) by A19, A57, Th51, TOPREAL1:10;
hence ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 & p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) by A57, A58, TOPREAL1:10, XXREAL_0:2; :: thesis: verum
end;
suppose p in Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C) ; :: thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
hence ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 & p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) by A19, A44, PSCOMP_1:71; :: thesis: verum
end;
suppose A59: p in LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| ; :: thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
A60: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= (LMP C) `2 by A19, Th53;
hence |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 by A59, TOPREAL1:10; :: thesis: p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2
p `2 <= (LMP C) `2 by A59, A60, TOPREAL1:10;
hence p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by A19, Th54, XXREAL_0:2; :: thesis: verum
end;
end;
end;
now
let p be Point of (TOP-REAL 2); :: thesis: ( p in ((LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) \/ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))) \/ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) implies ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 ) )
assume A61: p in ((LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) \/ (Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))) \/ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ; :: thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
per cases ( p in LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C) or p in Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C) or p in LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| ) by A61, Lm3;
suppose p in LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C) ; :: thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
then p `1 = (UMP C) `1 by A22, A24, SPPOL_1:def 3;
hence ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A15, A20, A21, A26, XREAL_1:228; :: thesis: verum
end;
suppose p in Segment (Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C) ; :: thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
hence ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A20, A21, A44, PSCOMP_1:71; :: thesis: verum
end;
suppose p in LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| ; :: thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
then p `1 = (LMP C) `1 by A23, A25, SPPOL_1:def 3;
hence ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A16, A20, A21, A26, XREAL_1:228; :: thesis: verum
end;
end;
end;
hence contradiction by A11, A28, A29, A49, A54, A55, JGRAPH_1:62; :: thesis: verum
end;
suppose LE UMP C, LMP C,C ; :: thesis: contradiction
then A62: LE UMP C, LMP C, Lower_Arc C, E-max C, W-min C by A13, JORDAN6:def 10;
set S = Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C);
A63: UMP C in Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C) by A12, A62, JORDAN16:9;
A64: LMP C in Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C) by A12, A62, JORDAN16:9;
A65: Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C) c= Lower_Arc C by JORDAN16:5;
then A66: Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C) c= C by A10, XBOOLE_1:1;
A67: (LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) = {(UMP C)}
proof
(LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) /\ C = {(UMP C)} by Th47;
hence (LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) c= {(UMP C)} by A66, XBOOLE_1:26; :: according to XBOOLE_0:def 10 :: thesis: {(UMP C)} c= (LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(UMP C)} or x in (LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) )
assume x in {(UMP C)} ; :: thesis: x in (LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))
then A68: x = UMP C by TARSKI:def 1;
UMP C in LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C) by RLTOPSP1:69;
hence x in (LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) by A63, A68, XBOOLE_0:def 4; :: thesis: verum
end;
A69: (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) = {(LMP C)}
proof
(LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) /\ C = {(LMP C)} by Th48;
hence (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) c= {(LMP C)} by A66, XBOOLE_1:26; :: according to XBOOLE_0:def 10 :: thesis: {(LMP C)} c= (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(LMP C)} or x in (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) )
assume x in {(LMP C)} ; :: thesis: x in (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))
then x = LMP C by TARSKI:def 1;
hence x in (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) /\ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) by A25, A64, XBOOLE_0:def 4; :: thesis: verum
end;
A70: ((LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) \/ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))) /\ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) = ((LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) /\ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) \/ ((Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) /\ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) by XBOOLE_1:23
.= {} \/ ((Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) /\ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) by A27, XBOOLE_0:def 7 ;
Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C) is_an_arc_of UMP C, LMP C by A12, A62, Th50, JORDAN16:36;
then (LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) \/ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) is_an_arc_of |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|, LMP C by A67, TOPREAL1:17;
then ((LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) \/ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))) \/ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) is_an_arc_of |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| by A69, A70, TOPREAL1:16;
then A71: ((LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) \/ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))) \/ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) is_an_arc_of |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| by JORDAN5B:14;
A72: Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C) c= (Lower_Arc C) \ {(W-min C),(E-max C)}
proof
let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C) or s in (Lower_Arc C) \ {(W-min C),(E-max C)} )
assume A73: s in Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C) ; :: thesis: s in (Lower_Arc C) \ {(W-min C),(E-max C)}
now
assume s in {(W-min C),(E-max C)} ; :: thesis: contradiction
then ( s = W-min C or s = E-max C ) by TARSKI:def 2;
hence contradiction by A4, A5, A12, A73, Th11; :: thesis: verum
end;
hence s in (Lower_Arc C) \ {(W-min C),(E-max C)} by A65, A73, XBOOLE_0:def 5; :: thesis: verum
end;
Upper_Arc C misses Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)
proof
assume Upper_Arc C meets Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C) ; :: thesis: contradiction
then consider x being set such that
A74: x in Upper_Arc C and
A75: x in Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C) by XBOOLE_0:3;
x in Lower_Arc C by A72, A75, XBOOLE_0:def 5;
then x in (Lower_Arc C) /\ (Upper_Arc C) by A74, XBOOLE_0:def 4;
hence contradiction by A8, A72, A75, XBOOLE_0:def 5; :: thesis: verum
end;
then A76: Upper_Arc C misses ((LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) \/ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))) \/ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) by A30, A35, Lm4;
A77: now
let p be Point of (TOP-REAL 2); :: thesis: ( p in ((LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) \/ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))) \/ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) implies ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) )
assume A78: p in ((LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) \/ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))) \/ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ; :: thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
per cases ( p in LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C) or p in Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C) or p in LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| ) by A78, Lm3;
suppose A79: p in LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C) ; :: thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
A80: (UMP C) `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by A19, Th52;
then ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= (UMP C) `2 & (UMP C) `2 <= p `2 ) by A19, A79, Th51, TOPREAL1:10;
hence ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 & p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) by A79, A80, TOPREAL1:10, XXREAL_0:2; :: thesis: verum
end;
suppose p in Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C) ; :: thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
hence ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 & p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) by A19, A66, PSCOMP_1:71; :: thesis: verum
end;
suppose A81: p in LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| ; :: thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
A82: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= (LMP C) `2 by A19, Th53;
hence |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 by A81, TOPREAL1:10; :: thesis: p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2
p `2 <= (LMP C) `2 by A81, A82, TOPREAL1:10;
hence p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by A19, Th54, XXREAL_0:2; :: thesis: verum
end;
end;
end;
now
let p be Point of (TOP-REAL 2); :: thesis: ( p in ((LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) \/ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))) \/ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) implies ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 ) )
assume A83: p in ((LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) \/ (Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))) \/ (LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ; :: thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
per cases ( p in LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C) or p in Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C) or p in LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| ) by A83, Lm3;
suppose p in LSeg |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C) ; :: thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
then p `1 = (UMP C) `1 by A22, A24, SPPOL_1:def 3;
hence ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A15, A20, A21, A26, XREAL_1:228; :: thesis: verum
end;
suppose p in Segment (Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C) ; :: thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
hence ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A20, A21, A66, PSCOMP_1:71; :: thesis: verum
end;
suppose p in LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| ; :: thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
then p `1 = (LMP C) `1 by A23, A25, SPPOL_1:def 3;
hence ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A16, A20, A21, A26, XREAL_1:228; :: thesis: verum
end;
end;
end;
hence contradiction by A11, A28, A29, A71, A76, A77, JGRAPH_1:62; :: thesis: verum
end;
end;