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