let C be Simple_closed_curve; :: thesis: ( not LMP C in Lower_Arc C or not UMP C in Lower_Arc C )
assume that
A1: LMP C in Lower_Arc C and
A2: UMP C in Lower_Arc C ; :: thesis: contradiction
A3: (Upper_Arc C) /\ (Lower_Arc C) = {(W-min C),(E-max C)} by JORDAN6:def 9;
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));
A4: Lower_Arc C c= C by JORDAN6:61;
A5: |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 = N-bound C by EUCLID:52;
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)]|);
A6: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:def 9;
A7: ( (W-min C) `1 = W-bound C & (E-max C) `1 = E-bound C ) by EUCLID:52;
A8: Upper_Arc C c= C by JORDAN6:61;
then A9: 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 A7, PSCOMP_1:24;
A10: UMP C <> E-max C by Th25;
A11: UMP C <> W-min C by Th24;
A12: now :: thesis: not UMP C in Upper_Arc C
assume UMP C in Upper_Arc C ; :: thesis: contradiction
then UMP C in (Upper_Arc C) /\ (Lower_Arc C) by A2, XBOOLE_0:def 4;
hence contradiction by A11, A10, A3, TARSKI:def 2; :: thesis: verum
end;
A13: W-bound C < E-bound C by SPRECT_1:31;
A14: Upper_Arc C misses LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))
proof
A15: (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ C = {(UMP C)} by Th34;
assume Upper_Arc C meets LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) ; :: thesis: contradiction
then consider x being object such that
A16: x in Upper_Arc C and
A17: 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 A8, A16, A17, XBOOLE_0:def 4;
then A18: x = UMP C by A15, TARSKI:def 1;
then x in (Lower_Arc C) /\ (Upper_Arc C) by A2, A16, XBOOLE_0:def 4;
hence contradiction by A11, A10, A3, A18, TARSKI:def 2; :: thesis: verum
end;
A19: ( UMP C in C & LMP C in C ) by Th30, Th31;
A20: (UMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
then A21: LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) is vertical by A20, SPPOL_1:16;
A22: UMP C in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) by RLTOPSP1:68;
A23: LMP C <> E-max C by Th27;
A24: LMP C <> W-min C by Th26;
A25: now :: thesis: not LMP C in Upper_Arc C
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 A24, A23, A3, TARSKI:def 2; :: thesis: verum
end;
A26: LMP C <> UMP C by Th37;
A27: (LMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A28: Upper_Arc C misses LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)
proof
A29: (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ C = {(LMP C)} by Th35;
assume Upper_Arc C meets LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ; :: thesis: contradiction
then consider x being object such that
A30: x in Upper_Arc C and
A31: 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 A8, A30, A31, XBOOLE_0:def 4;
then A32: x = LMP C by A29, TARSKI:def 1;
then x in (Lower_Arc C) /\ (Upper_Arc C) by A1, A30, XBOOLE_0:def 4;
hence contradiction by A24, A23, A3, A32, 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:52;
then A33: LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) is vertical by A27, SPPOL_1:16;
A34: LMP C in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) by RLTOPSP1:68;
A35: 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 Th42;
A36: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 = S-bound C by EUCLID:52;
then A37: ( Upper_Arc C is_an_arc_of W-min C, E-max C & ( 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 A8, A5, JORDAN6:def 8, PSCOMP_1:24;
per cases ( LE LMP C, UMP C,C or LE UMP C, LMP C,C ) by A19, JORDAN16:7;
suppose A38: LE LMP C, UMP C,C ; :: thesis: contradiction
set S = Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C));
A39: Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) c= Lower_Arc C by JORDAN16:2;
then A40: Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) c= C by A4;
A41: now :: thesis: for p being Point of (TOP-REAL 2) st 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)]|)) holds
( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 )
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 A42: 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 A42, 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 A21, A22, SPPOL_1:def 3;
hence ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A20, A7, A13, XREAL_1:226; :: 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 A7, A40, PSCOMP_1:24; :: 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 A33, A34, SPPOL_1:def 3;
hence ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A27, A7, A13, XREAL_1:226; :: thesis: verum
end;
end;
end;
A43: now :: thesis: for p being Point of (TOP-REAL 2) st 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)]|)) 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 )
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 A44: 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 A44, Lm3;
suppose A45: 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 )
A46: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= (UMP C) `2 by A36, Th38;
A47: (UMP C) `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by A5, Th39;
then (UMP C) `2 <= p `2 by A45, TOPREAL1:4;
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 A45, A47, A46, TOPREAL1:4, 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 A36, A5, A40, PSCOMP_1:24; :: thesis: verum
end;
suppose A48: 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 )
A49: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= (LMP C) `2 by A36, Th40;
hence |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 by A48, TOPREAL1:4; :: thesis: p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2
p `2 <= (LMP C) `2 by A48, A49, TOPREAL1:4;
hence p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by A5, Th41, XXREAL_0:2; :: thesis: verum
end;
end;
end;
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 object ; :: 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 :: thesis: not s in {(W-min C),(E-max C)}
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 A11, A23, A6, A51, Th11; :: thesis: verum
end;
hence s in (Lower_Arc C) \ {(W-min C),(E-max C)} by A39, 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 object 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 A3, 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 A14, A28, Lm4;
A55: LE LMP C, UMP C, Lower_Arc C, E-max C, W-min C by A25, A38, JORDAN6:def 10;
then A56: UMP C in Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) by JORDAN16:5;
A57: (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 Th34;
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 A40, 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 object ; :: 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 A58: 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:68;
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 A56, A58, XBOOLE_0:def 4; :: thesis: verum
end;
A59: LMP C in Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) by A55, JORDAN16:5;
A60: (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 Th35;
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 A40, 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 object ; :: 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 A34, A59, XBOOLE_0:def 4; :: thesis: verum
end;
Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) is_an_arc_of LMP C, UMP C by A26, A6, A55, JORDAN16:21;
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 A61: (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 A57, TOPREAL1:11;
((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 A35 ;
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 A60, A61, TOPREAL1:10;
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),(S-bound C)]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| by JORDAN5B:14;
hence contradiction by A37, A9, A54, A43, A41, JGRAPH_1:44; :: thesis: verum
end;
suppose A62: LE UMP C, LMP C,C ; :: thesis: contradiction
set S = Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C));
A63: Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) c= Lower_Arc C by JORDAN16:2;
then A64: Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) c= C by A4;
A65: now :: thesis: for p being Point of (TOP-REAL 2) st 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)]|)) holds
( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 )
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 A66: 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 A66, 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 A21, A22, SPPOL_1:def 3;
hence ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A20, A7, A13, XREAL_1:226; :: 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 A7, A64, PSCOMP_1:24; :: 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 A33, A34, SPPOL_1:def 3;
hence ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A27, A7, A13, XREAL_1:226; :: thesis: verum
end;
end;
end;
A67: now :: thesis: for p being Point of (TOP-REAL 2) st 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)]|)) 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 )
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 A68: 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 A68, Lm3;
suppose A69: 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 )
A70: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= (UMP C) `2 by A36, Th38;
A71: (UMP C) `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by A5, Th39;
then (UMP C) `2 <= p `2 by A69, TOPREAL1:4;
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 A69, A71, A70, TOPREAL1:4, 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 A36, A5, A64, PSCOMP_1:24; :: thesis: verum
end;
suppose A72: 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 )
A73: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= (LMP C) `2 by A36, Th40;
hence |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 by A72, TOPREAL1:4; :: thesis: p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2
p `2 <= (LMP C) `2 by A72, A73, TOPREAL1:4;
hence p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by A5, Th41, XXREAL_0:2; :: thesis: verum
end;
end;
end;
A74: 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 object ; :: 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 A75: 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 :: thesis: not s in {(W-min C),(E-max C)}
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 A10, A24, A6, A75, Th11; :: thesis: verum
end;
hence s in (Lower_Arc C) \ {(W-min C),(E-max C)} by A63, A75, 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 object such that
A76: x in Upper_Arc C and
A77: 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 A74, A77, XBOOLE_0:def 5;
then x in (Lower_Arc C) /\ (Upper_Arc C) by A76, XBOOLE_0:def 4;
hence contradiction by A3, A74, A77, XBOOLE_0:def 5; :: thesis: verum
end;
then A78: 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 A14, A28, Lm4;
A79: LE UMP C, LMP C, Lower_Arc C, E-max C, W-min C by A12, A62, JORDAN6:def 10;
then A80: UMP C in Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) by JORDAN16:5;
A81: (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 Th34;
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 A64, 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 object ; :: 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 A82: 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:68;
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 A80, A82, XBOOLE_0:def 4; :: thesis: verum
end;
A83: LMP C in Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) by A79, JORDAN16:5;
A84: (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 Th35;
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 A64, 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 object ; :: 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 A34, A83, XBOOLE_0:def 4; :: thesis: verum
end;
Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) is_an_arc_of UMP C, LMP C by A6, A79, Th37, JORDAN16:21;
then A85: (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 A81, TOPREAL1:11;
((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 A35 ;
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 A84, A85, TOPREAL1:10;
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),(S-bound C)]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| by JORDAN5B:14;
hence contradiction by A37, A9, A78, A67, A65, JGRAPH_1:44; :: thesis: verum
end;
end;