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 Th30, Th31;
A7: (UMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
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:61;
A9: |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 = N-bound C 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 A10: LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) is vertical by A7, SPPOL_1:16;
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 Th42;
A12: UMP C in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) by RLTOPSP1:68;
A13: ( (W-min C) `1 = W-bound C & (E-max C) `1 = E-bound C ) by EUCLID:52;
A14: Lower_Arc C c= C by JORDAN6:61;
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:24;
A16: UMP C <> E-max C by Th25;
A17: UMP C <> W-min C by Th24;
A18: now :: thesis: not UMP C in Lower_Arc C
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:31;
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 Th34;
assume Lower_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
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 Th27;
A26: LMP C <> W-min C by Th26;
A27: now :: thesis: not LMP C in Lower_Arc C
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 Th37;
A29: (LMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
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 Th35;
assume Lower_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
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:52;
then A35: LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) is vertical by A29, SPPOL_1:16;
A36: LMP C in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) by RLTOPSP1:68;
A37: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 = S-bound C by EUCLID:52;
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:24;
per cases ( LE LMP C, UMP C,C or LE UMP C, LMP C,C ) by A6, JORDAN16:7;
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:2;
then A41: Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)) c= C by A8;
A42: 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 ((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)]|)) 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 ((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:226; :: 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: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 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:226; :: thesis: verum
end;
end;
end;
A44: 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 ((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)]|)) 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 ((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, Th38;
A48: (UMP C) `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by A9, Th39;
then (UMP C) `2 <= p `2 by A46, 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 A46, A48, A47, TOPREAL1:4, 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:24; :: 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, Th40;
hence |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 by A49, TOPREAL1:4; :: thesis: p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2
p `2 <= (LMP C) `2 by A49, A50, TOPREAL1:4;
hence p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by A9, Th41, 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 object ; :: 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 :: 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 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 object 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:5;
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 Th34;
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 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 ((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:68;
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:5;
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 Th35;
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 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 ((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:21;
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:11;
((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 ;
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:10;
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:44; :: 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:2;
then A65: Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)) c= C by A8;
A66: 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 ((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)]|)) 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 ((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:226; :: 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: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 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:226; :: thesis: verum
end;
end;
end;
A68: 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 ((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)]|)) 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 ((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, Th38;
A72: (UMP C) `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by A9, Th39;
then (UMP C) `2 <= p `2 by A70, 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 A70, A72, A71, TOPREAL1:4, 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:24; :: 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, Th40;
hence |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 by A73, TOPREAL1:4; :: thesis: p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2
p `2 <= (LMP C) `2 by A73, A74, TOPREAL1:4;
hence p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by A9, Th41, 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 object ; :: 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 :: 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 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 object 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:5;
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 Th34;
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 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 ((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:68;
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:5;
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 Th35;
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 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 ((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, Th37, JORDAN16:21;
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:11;
((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 ;
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:10;
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:44; :: thesis: verum
end;
end;