let C be Simple_closed_curve; :: thesis: ( |[(- 1),0]|,|[1,0]| realize-max-dist-in C implies for Jc, Jd being compact with_the_max_arc Subset of (TOP-REAL 2) st Jc is_an_arc_of |[(- 1),0]|,|[1,0]| & Jd is_an_arc_of |[(- 1),0]|,|[1,0]| & C = Jc \/ Jd & Jc /\ Jd = {|[(- 1),0]|,|[1,0]|} & UMP C in Jc & LMP C in Jd & W-bound C = W-bound Jc & E-bound C = E-bound Jc holds
for Ux being Subset of (TOP-REAL 2) st Ux = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) holds
( Ux is_inside_component_of C & ( for V being Subset of (TOP-REAL 2) st V is_inside_component_of C holds
V = Ux ) ) )
set m = UMP C;
set j = LMP C;
assume A1: |[(- 1),0]|,|[1,0]| realize-max-dist-in C ; :: thesis: for Jc, Jd being compact with_the_max_arc Subset of (TOP-REAL 2) st Jc is_an_arc_of |[(- 1),0]|,|[1,0]| & Jd is_an_arc_of |[(- 1),0]|,|[1,0]| & C = Jc \/ Jd & Jc /\ Jd = {|[(- 1),0]|,|[1,0]|} & UMP C in Jc & LMP C in Jd & W-bound C = W-bound Jc & E-bound C = E-bound Jc holds
for Ux being Subset of (TOP-REAL 2) st Ux = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) holds
( Ux is_inside_component_of C & ( for V being Subset of (TOP-REAL 2) st V is_inside_component_of C holds
V = Ux ) )
let Jc, Jd be compact with_the_max_arc Subset of (TOP-REAL 2); :: thesis: ( Jc is_an_arc_of |[(- 1),0]|,|[1,0]| & Jd is_an_arc_of |[(- 1),0]|,|[1,0]| & C = Jc \/ Jd & Jc /\ Jd = {|[(- 1),0]|,|[1,0]|} & UMP C in Jc & LMP C in Jd & W-bound C = W-bound Jc & E-bound C = E-bound Jc implies for Ux being Subset of (TOP-REAL 2) st Ux = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) holds
( Ux is_inside_component_of C & ( for V being Subset of (TOP-REAL 2) st V is_inside_component_of C holds
V = Ux ) ) )
assume that
A2: Jc is_an_arc_of |[(- 1),0]|,|[1,0]| and
A3: Jd is_an_arc_of |[(- 1),0]|,|[1,0]| and
A4: C = Jc \/ Jd and
A5: Jc /\ Jd = {|[(- 1),0]|,|[1,0]|} and
A6: UMP C in Jc and
A7: LMP C in Jd and
A8: W-bound C = W-bound Jc and
A9: E-bound C = E-bound Jc ; :: thesis: for Ux being Subset of (TOP-REAL 2) st Ux = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) holds
( Ux is_inside_component_of C & ( for V being Subset of (TOP-REAL 2) st V is_inside_component_of C holds
V = Ux ) )
set l = LMP Jc;
set LJ = (LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd;
set k = UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd);
set x = (1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc));
set w = ((W-bound C) + (E-bound C)) / 2;
let Ux be Subset of (TOP-REAL 2); :: thesis: ( Ux = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) implies ( Ux is_inside_component_of C & ( for V being Subset of (TOP-REAL 2) st V is_inside_component_of C holds
V = Ux ) ) )
assume A10: Ux = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) ; :: thesis: ( Ux is_inside_component_of C & ( for V being Subset of (TOP-REAL 2) st V is_inside_component_of C holds
V = Ux ) )
A11: C c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A1, Th71;
A12: W-bound C = - 1 by A1, Th75;
A13: E-bound C = 1 by A1, Th76;
A14: |[(- 1),0]| in C by A1, JORDAN24:def 1;
A15: |[1,0]| in C by A1, JORDAN24:def 1;
A16: UMP C in C by JORDAN21:30;
A17: LMP Jc in Jc by JORDAN21:31;
A18: Jd c= C by A4, XBOOLE_1:7;
A19: Jc c= C by A4, XBOOLE_1:7;
then A20: LMP Jc in C by A17;
A21: (UMP C) `2 < |[0,3]| `2 by A1, Lm21, Th83, JORDAN21:30;
A22: (LMP Jc) `1 = 0 by A8, A9, A12, A13, EUCLID:52;
A23: |[0,3]| `1 = ((W-bound C) + (E-bound C)) / 2 by A1, Lm87;
A24: (UMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A25: UMP C <> |[(- 1),0]| by A12, A13, Lm16, EUCLID:52;
A26: UMP C <> |[1,0]| by A12, A13, Lm17, EUCLID:52;
A27: LMP Jc <> |[(- 1),0]| by A8, A9, A12, A13, Lm16, EUCLID:52;
A28: LMP Jc <> |[1,0]| by A8, A9, A12, A13, Lm17, EUCLID:52;
then consider Pml being Path of UMP C, LMP Jc such that
A29: rng Pml c= Jc and
A30: rng Pml misses {|[(- 1),0]|,|[1,0]|} by A2, A6, A17, A25, A26, A27, Th44;
set ml = rng Pml;
A31: rng Pml c= C by A19, A29, XBOOLE_1:1;
A32: LMP C in C by A7, A18;
A33: LSeg ((LMP Jc),|[0,(- 3)]|) is vertical by A22, Lm22, SPPOL_1:16;
A34: |[0,(- 3)]| `2 <= (LMP C) `2 by A1, A7, A18, Lm23, Th84;
A35: (LMP C) `1 = 0 by A12, A13, EUCLID:52;
LMP Jc in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A12, A13, A22, JORDAN6:31;
then A36: LMP Jc in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) by A17, A19, XBOOLE_0:def 4;
then (LMP C) `2 <= (LMP Jc) `2 by JORDAN21:29;
then LMP C in LSeg ((LMP Jc),|[0,(- 3)]|) by A22, A34, A35, Lm22, GOBOARD7:7;
then A37: not (LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd is empty by A7, XBOOLE_0:def 4;
A39: (LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd is vertical by A33, Th4;
then A40: UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) in (LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd by A37, JORDAN21:30;
then A41: UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) in LSeg ((LMP Jc),|[0,(- 3)]|) by XBOOLE_0:def 4;
A42: UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) in Jd by A40, XBOOLE_0:def 4;
then A43: UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) in C by A18;
A44: |[0,(- 3)]| in LSeg ((LMP Jc),|[0,(- 3)]|) by RLTOPSP1:68;
then A45: (UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `1 = 0 by A33, A41, Lm22, SPPOL_1:def 3;
then A46: UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) <> |[(- 1),0]| by EUCLID:52;
A47: UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) <> |[1,0]| by A45, EUCLID:52;
A48: LMP C <> |[(- 1),0]| by A35, EUCLID:52;
LMP C <> |[1,0]| by A35, EUCLID:52;
then consider Pkj being Path of UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd), LMP C such that
A49: rng Pkj c= Jd and
A50: rng Pkj misses {|[(- 1),0]|,|[1,0]|} by A3, A7, A42, A46, A47, A48, Th44;
set kj = rng Pkj;
A51: rng Pkj c= C by A18, A49, XBOOLE_1:1;
A52: (1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)) in LSeg ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)),(LMP Jc)) by RLTOPSP1:69;
A53: Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) is a_component by CONNSP_1:40;
A54: the carrier of ((TOP-REAL 2) | (C `)) = C ` by PRE_TOPC:8;
A55: LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) is vertical by A22, A45, SPPOL_1:16;
A56: UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) in LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) by RLTOPSP1:68;
A57: LMP Jc = |[((LMP Jc) `1),((LMP Jc) `2)]| by EUCLID:53;
A58: UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) = |[((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `1),((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `2)]| by EUCLID:53;
A59: |[0,(- 3)]| = |[(|[0,(- 3)]| `1),(|[0,(- 3)]| `2)]| by EUCLID:53;
|[0,(- 3)]| `2 <= (LMP Jc) `2 by A1, A17, A19, Lm23, Th84;
then A60: (UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `2 <= (LMP Jc) `2 by A22, A41, A57, A59, Lm22, JGRAPH_6:1;
A61: |[(- 1),0]| <> UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) by A45, EUCLID:52;
|[1,0]| <> UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) by A45, EUCLID:52;
then not UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) in {|[(- 1),0]|,|[1,0]|} by A61, TARSKI:def 2;
then A62: UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) <> LMP Jc by A5, A17, A42, XBOOLE_0:def 4;
then (UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `2 <> (LMP Jc) `2 by A22, A45, TOPREAL3:6;
then A63: (UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `2 < (LMP Jc) `2 by A60, XXREAL_0:1;
UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A12, A13, A45, JORDAN6:31;
then UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) by A18, A42, XBOOLE_0:def 4;
then (LMP C) `2 <= (UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `2 by JORDAN21:29;
then |[0,(- 3)]| `2 <= (UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `2 by A1, A7, A18, Lm23, Th84, XXREAL_0:2;
then A64: LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) c= LSeg ((LMP Jc),|[0,(- 3)]|) by A33, A45, A55, A60, Lm22, GOBOARD7:63;
A65: (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) \ {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} c= C `

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) \ {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} or q in C ` )
assume that
A66: q in (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) \ {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} and
A67: not q in C ` ; :: thesis: contradiction
A68: q in LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) by A66, XBOOLE_0:def 5;
reconsider q = q as Point of (TOP-REAL 2) by A66;
A69: q in C by A67, SUBSET_1:29;
A70: q `1 = ((W-bound C) + (E-bound C)) / 2 by A12, A13, A45, A55, A56, A68, SPPOL_1:def 3;
then A71: q in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by JORDAN6:31;

per cases ( q in Jc or q in Jd ) by A4, A69, XBOOLE_0:def 3;

suppose q in Jc ; :: thesis: contradiction

then q in Jc /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) by A71, XBOOLE_0:def 4;
then A72: (LMP Jc) `2 <= q `2 by A8, A9, JORDAN21:29;
q `2 <= (LMP Jc) `2 by A22, A45, A57, A58, A60, A68, JGRAPH_6:1;
then (LMP Jc) `2 = q `2 by A72, XXREAL_0:1;
then LMP Jc = q by A12, A13, A22, A70, TOPREAL3:6;
then q in {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} by TARSKI:def 2;
hence contradiction by A66, XBOOLE_0:def 5; :: thesis: verum

end;

suppose q in Jd ; :: thesis: contradiction

then A73: q in (LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd by A64, A68, XBOOLE_0:def 4;
A74: q `1 = |[0,(- 3)]| `1 by A33, A44, A64, A68, SPPOL_1:def 3;
A75: W-bound (LSeg ((LMP Jc),|[0,(- 3)]|)) <= W-bound ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) by A73, PSCOMP_1:69, XBOOLE_1:17;
A76: E-bound ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) <= E-bound (LSeg ((LMP Jc),|[0,(- 3)]|)) by A73, PSCOMP_1:67, XBOOLE_1:17;
A77: W-bound ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) = E-bound ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) by A37, A39, SPRECT_1:15;
A78: W-bound (LSeg ((LMP Jc),|[0,(- 3)]|)) = |[0,(- 3)]| `1 by A22, Lm22, SPRECT_1:54;
then W-bound (LSeg ((LMP Jc),|[0,(- 3)]|)) = W-bound ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) by A22, A75, A76, A77, Lm22, SPRECT_1:57;
then q in Vertical_Line (((W-bound ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (E-bound ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) / 2) by A74, A77, A78, JORDAN6:31;
then q in ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) /\ (Vertical_Line (((W-bound ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (E-bound ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) / 2)) by A73, XBOOLE_0:def 4;
then A79: q `2 <= (UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `2 by JORDAN21:28;
(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `2 <= q `2 by A22, A45, A57, A58, A60, A68, JGRAPH_6:1;
then (UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `2 = q `2 by A79, XXREAL_0:1;
then UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) = q by A12, A13, A45, A70, TOPREAL3:6;
then q in {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} by TARSKI:def 2;
hence contradiction by A66, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

then reconsider X = (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) \ {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} as Subset of ((TOP-REAL 2) | (C `)) by PRE_TOPC:8;

now

assume (1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)) in {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} ; :: thesis: contradiction
then ( (1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)) = LMP Jc or (1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)) = UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) ) by TARSKI:def 2;
hence contradiction by A62, Th1; :: thesis: verum

end;

then A80: (1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)) in (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) \ {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} by A52, XBOOLE_0:def 5;
then Component_of (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `)) = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) by A65, CONNSP_3:27;
then A81: (1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)) in Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) by A65, A80, CONNSP_3:26;
then A82: X meets Ux by A10, A80, XBOOLE_0:3;
(LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) \ {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} is connected by JORDAN1:47;
then X is connected by CONNSP_1:23;
then A83: X c= Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) by A10, A53, A82, CONNSP_1:36;
A84: LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A11, A20, A43, JORDAN1:def 1;
A85: the carrier of (Trectangle ((- 1),1,(- 3),3)) = closed_inside_of_rectangle ((- 1),1,(- 3),3) by PRE_TOPC:8;
reconsider AR = |[(- 1),0]|, BR = |[1,0]|, CR = |[0,3]|, DR = |[0,(- 3)]| as Point of (Trectangle ((- 1),1,(- 3),3)) by A11, A14, A15, Lm62, Lm63, Lm67, PRE_TOPC:8;
consider Pcm being Path of |[0,3]|, UMP C, fcm being Function of I[01],((TOP-REAL 2) | (LSeg (|[0,3]|,(UMP C)))) such that
A86: rng fcm = LSeg (|[0,3]|,(UMP C)) and
A87: Pcm = fcm by Th43;
A88: LSeg (|[0,3]|,(UMP C)) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A11, A16, Lm62, Lm67, JORDAN1:def 1;
A89: rng Pml c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A11, A31, XBOOLE_1:1;
thus Ux is_inside_component_of C :: thesis: for V being Subset of (TOP-REAL 2) st V is_inside_component_of C holds
V = Ux

proof

thus A90: Ux is_a_component_of C ` by A10, A53, CONNSP_1:def 6; :: according to JORDAN2C:def 2 :: thesis: Ux is Bounded
assume not Ux is Bounded ; :: thesis: contradiction
then not Ux c= Ball (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),10) by JORDAN2C:12;
then consider u being set such that
A91: u in Ux and
A92: not u in Ball (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),10) by TARSKI:def 3;
A93: closed_inside_of_rectangle ((- 1),1,(- 3),3) c= Ball (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),10) by A52, A84, Lm89;
reconsider u = u as Point of (TOP-REAL 2) by A91;
A94: Ux is open by A90, SPRECT_3:8;
Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) is connected by A53, CONNSP_1:def 5;
then A95: Ux is connected by A10, CONNSP_1:23;
(1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)) in Ball (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),10) by Th16;
then consider P1 being Subset of (TOP-REAL 2) such that
A96: P1 is_S-P_arc_joining (1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)),u and
A97: P1 c= Ux by A10, A81, A91, A92, A94, A95, TOPREAL4:29;
A98: P1 is_an_arc_of (1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)),u by A96, TOPREAL4:2;
reconsider P2 = P1 as Subset of ((TOP-REAL 2) | (C `)) by A10, A97, XBOOLE_1:1;
A99: P2 c= Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) by A10, A97;
A100: P2 misses C by A54, SUBSET_1:23;
then A101: P2 misses Jc by A4, XBOOLE_1:7, XBOOLE_1:63;
A102: P2 misses Jd by A4, A100, XBOOLE_1:7, XBOOLE_1:63;
A103: ((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))) `1 = (1 / 2) * (((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)) `1) by TOPREAL3:4
.= (1 / 2) * (((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `1) + ((LMP Jc) `1)) by TOPREAL3:2
.= 0 by A22, A45 ;
then A104: LSeg (|[0,(- 3)]|,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) is vertical by Lm22, SPPOL_1:16;
A105: (1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)) = |[(((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))) `1),(((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))) `2)]| by EUCLID:53;
A106: ((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))) `2 < (LMP Jc) `2 by A63, Th3;
A107: (UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `2 < ((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))) `2 by A63, Th2;
then A108: |[0,(- 3)]| `2 <= ((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))) `2 by A1, A18, A42, Lm23, Th84, XXREAL_0:2;
|[0,(- 3)]| `1 = |[0,(- 3)]| `1 ;
then A109: LSeg (|[0,(- 3)]|,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) c= LSeg (|[0,(- 3)]|,(LMP Jc)) by A33, A104, A106, A108, GOBOARD7:63;
A110: LSeg (|[0,(- 3)]|,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) misses Jc

proof

assume not LSeg (|[0,(- 3)]|,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) misses Jc ; :: thesis: contradiction
then consider q being set such that
A111: q in LSeg (|[0,(- 3)]|,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) and
A112: q in Jc by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A111;
q `2 <= ((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))) `2 by A59, A103, A105, A108, A111, Lm22, JGRAPH_6:1;
then A113: q `2 < (LMP Jc) `2 by A106, XXREAL_0:2;
q `1 = 0 by A33, A44, A109, A111, Lm22, SPPOL_1:def 3;
then q in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A12, A13, JORDAN6:31;
then q in Jc /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) by A112, XBOOLE_0:def 4;
hence contradiction by A8, A9, A113, JORDAN21:29; :: thesis: verum

end;

set n = First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)));
A114: not u in closed_inside_of_rectangle ((- 1),1,(- 3),3) by A92, A93;
A115: Fr (closed_inside_of_rectangle ((- 1),1,(- 3),3)) = rectangle ((- 1),1,(- 3),3) by Th52;
u in P1 by A98, TOPREAL1:1;
then A116: P1 \ (closed_inside_of_rectangle ((- 1),1,(- 3),3)) <> {} (TOP-REAL 2) by A114, XBOOLE_0:def 5;
(1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)) in P1 by A98, TOPREAL1:1;
then P1 meets closed_inside_of_rectangle ((- 1),1,(- 3),3) by A52, A84, XBOOLE_0:3;
then A117: P1 meets rectangle ((- 1),1,(- 3),3) by A98, A115, A116, CONNSP_1:22, JORDAN6:10;
P1 is closed by A96, JORDAN6:11, TOPREAL4:2;
then A118: First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in P1 /\ (rectangle ((- 1),1,(- 3),3)) by A98, A117, JORDAN5C:def 1;
then A119: First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in rectangle ((- 1),1,(- 3),3) by XBOOLE_0:def 4;
A120: First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in P1 by A118, XBOOLE_0:def 4;
set alpha = Segment (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))));
A121: - 3 < (UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `2 by A1, A18, A42, Th84;
(LMP Jc) `2 <= (UMP C) `2 by A36, JORDAN21:28;
then ((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))) `2 < (UMP C) `2 by A106, XXREAL_0:2;
then not (1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)) in rectangle ((- 1),1,(- 3),3) by A21, A103, A105, A107, A121, Lm86;
then A122: Segment (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))))) is_an_arc_of (1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)), First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) by A96, A119, A120, JORDAN16:24, TOPREAL4:2;
A123: Segment (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))))) misses Jc by A101, JORDAN16:2, XBOOLE_1:63;
A124: Segment (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))))) misses Jd by A102, JORDAN16:2, XBOOLE_1:63;
consider Pdx being Path of |[0,(- 3)]|,(1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)), fdx being Function of I[01],((TOP-REAL 2) | (LSeg (|[0,(- 3)]|,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))))) such that
A125: rng fdx = LSeg (|[0,(- 3)]|,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) and
A126: Pdx = fdx by Th43;
consider PJc being Path of |[(- 1),0]|,|[1,0]|, fJc being Function of I[01],((TOP-REAL 2) | Jc) such that
A127: rng fJc = Jc and
A128: PJc = fJc by A2, Th42;
consider PJd being Path of |[(- 1),0]|,|[1,0]|, fJd being Function of I[01],((TOP-REAL 2) | Jd) such that
A129: rng fJd = Jd and
A130: PJd = fJd by A3, Th42;
consider Palpha being Path of (1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)), First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))), falpha being Function of I[01],((TOP-REAL 2) | (Segment (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))))))) such that
A131: rng falpha = Segment (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))))) and
A132: Palpha = falpha by A122, Th42;
First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in closed_inside_of_rectangle ((- 1),1,(- 3),3) by A119, Lm67;
then A133: ex p being Point of (TOP-REAL 2) st
( p = First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) & - 1 <= p `1 & p `1 <= 1 & - 3 <= p `2 & p `2 <= 3 ) ;
rng PJc c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A11, A19, A85, A127, A128, XBOOLE_1:1;
then reconsider h = PJc as Path of AR,BR by Th30;
rng PJd c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A11, A18, A85, A129, A130, XBOOLE_1:1;
then reconsider H = PJd as Path of AR,BR by Th30;
A134: LSeg (|[0,(- 3)]|,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A52, A84, Lm63, Lm67, JORDAN1:def 1;
A135: Segment (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))))) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A52, A84, A96, A114, Th57, TOPREAL4:2;
A136: |[(- 1),(- 3)]| in LSeg (|[(- 1),(- 3)]|,|[(- 1),3]|) by RLTOPSP1:68;
A137: |[1,(- 3)]| in LSeg (|[1,(- 3)]|,|[1,3]|) by RLTOPSP1:68;
LSeg (|[(- 1),3]|,|[0,3]|) misses C by A1, Lm78;
then A138: LSeg (|[(- 1),3]|,|[0,3]|) misses Jc by A4, XBOOLE_1:7, XBOOLE_1:63;
A139: LSeg (|[(- 1),3]|,|[0,3]|) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by Lm67, Lm70, XBOOLE_1:1;
A140: LSeg (|[1,3]|,|[0,3]|) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by Lm67, Lm71, XBOOLE_1:1;
LSeg (|[1,3]|,|[0,3]|) misses C by A1, Lm79;
then A141: LSeg (|[1,3]|,|[0,3]|) misses Jc by A4, XBOOLE_1:7, XBOOLE_1:63;
consider Plx being Path of LMP Jc,(1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)), flx being Function of I[01],((TOP-REAL 2) | (LSeg ((LMP Jc),((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))))) such that
A142: rng flx = LSeg ((LMP Jc),((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) and
A143: Plx = flx by Th43;
set PCX = (Pcm + Pml) + Plx;
A144: rng ((Pcm + Pml) + Plx) = ((rng Pcm) \/ (rng Pml)) \/ (rng Plx) by Th40;
A145: rng Pml misses Jd

proof

assume rng Pml meets Jd ; :: thesis: contradiction
then consider q being set such that
A146: q in rng Pml and
A147: q in Jd by XBOOLE_0:3;
q in {|[(- 1),0]|,|[1,0]|} by A5, A29, A146, A147, XBOOLE_0:def 4;
hence contradiction by A30, A146, XBOOLE_0:3; :: thesis: verum

end;

A148: (LSeg (|[0,3]|,(UMP C))) /\ C = {(UMP C)} by A1, Th91;
A149: LSeg (|[0,3]|,(UMP C)) misses Jd

proof

assume LSeg (|[0,3]|,(UMP C)) meets Jd ; :: thesis: contradiction
then consider q being set such that
A150: q in LSeg (|[0,3]|,(UMP C)) and
A151: q in Jd by XBOOLE_0:3;
q in {(UMP C)} by A18, A148, A150, A151, XBOOLE_0:def 4;
then q = UMP C by TARSKI:def 1;
then UMP C in {|[(- 1),0]|,|[1,0]|} by A5, A6, A151, XBOOLE_0:def 4;
hence contradiction by A25, A26, TARSKI:def 2; :: thesis: verum

end;

LSeg ((LMP Jc),((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) is vertical by A22, A103, SPPOL_1:16;
then A152: LSeg ((LMP Jc),((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) c= LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) by A45, A55, A103, A106, A107, GOBOARD7:63;
LMP Jc in LSeg ((LMP Jc),((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) by RLTOPSP1:68;
then {(LMP Jc)} c= LSeg ((LMP Jc),((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) by ZFMISC_1:31;
then A153: LSeg ((LMP Jc),((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) = ((LSeg ((LMP Jc),((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))))) \ {(LMP Jc)}) \/ {(LMP Jc)} by XBOOLE_1:45;
(LSeg ((LMP Jc),((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))))) \ {(LMP Jc)} c= (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) \ {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))}

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in (LSeg ((LMP Jc),((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))))) \ {(LMP Jc)} or q in (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) \ {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} )
assume A154: q in (LSeg ((LMP Jc),((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))))) \ {(LMP Jc)} ; :: thesis: q in (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) \ {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))}
then A155: q in LSeg ((LMP Jc),((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) by ZFMISC_1:56;
A156: q <> LMP Jc by A154, ZFMISC_1:56;
q <> UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) by A22, A57, A103, A105, A106, A107, A155, JGRAPH_6:1;
then not q in {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} by A156, TARSKI:def 2;
hence q in (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) \ {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} by A152, A155, XBOOLE_0:def 5; :: thesis: verum

end;

then (LSeg ((LMP Jc),((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))))) \ {(LMP Jc)} c= C ` by A65, XBOOLE_1:1;
then (LSeg ((LMP Jc),((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))))) \ {(LMP Jc)} misses C by SUBSET_1:23;
then A157: (LSeg ((LMP Jc),((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))))) \ {(LMP Jc)} misses Jd by A4, XBOOLE_1:7, XBOOLE_1:63;
{(LMP Jc)} misses Jd

proof

assume {(LMP Jc)} meets Jd ; :: thesis: contradiction
then LMP Jc in Jd by ZFMISC_1:50;
then LMP Jc in {|[(- 1),0]|,|[1,0]|} by A5, A17, XBOOLE_0:def 4;
hence contradiction by A27, A28, TARSKI:def 2; :: thesis: verum

end;

then LSeg ((LMP Jc),((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) misses Jd by A153, A157, XBOOLE_1:70;
then A158: rng ((Pcm + Pml) + Plx) misses Jd by A86, A87, A142, A143, A144, A145, A149, XBOOLE_1:114;
LSeg ((LMP Jc),((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A84, A152, XBOOLE_1:1;
then A159: rng ((Pcm + Pml) + Plx) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A86, A87, A88, A89, A142, A143, A144, Lm1;
LSeg (|[(- 1),(- 3)]|,|[0,(- 3)]|) misses C by A1, Lm80;
then A160: LSeg (|[(- 1),(- 3)]|,|[0,(- 3)]|) misses Jd by A4, XBOOLE_1:7, XBOOLE_1:63;
LSeg (|[1,(- 3)]|,|[0,(- 3)]|) misses C by A1, Lm81;
then A161: LSeg (|[1,(- 3)]|,|[0,(- 3)]|) misses Jd by A4, XBOOLE_1:7, XBOOLE_1:63;

per cases ( (First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))) `2 < 0 or (First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))) `2 >= 0 ) ;

suppose A162: (First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))) `2 < 0 ; :: thesis: contradiction

per cases ( First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in LSeg (|[(- 1),0]|,|[(- 1),(- 3)]|) or First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in LSeg (|[(- 1),(- 3)]|,|[0,(- 3)]|) or First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in LSeg (|[0,(- 3)]|,|[1,(- 3)]|) or First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in LSeg (|[1,(- 3)]|,|[1,0]|) ) by A119, A162, Lm77;

suppose A163: First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in LSeg (|[(- 1),0]|,|[(- 1),(- 3)]|) ; :: thesis: contradiction

consider Pnld being Path of First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))),|[(- 1),(- 3)]|, fnld being Function of I[01],((TOP-REAL 2) | (LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[(- 1),(- 3)]|))) such that
A164: rng fnld = LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[(- 1),(- 3)]|) and
A165: Pnld = fnld by Th43;
consider Pldd being Path of |[(- 1),(- 3)]|,|[0,(- 3)]|, fldd being Function of I[01],((TOP-REAL 2) | (LSeg (|[(- 1),(- 3)]|,|[0,(- 3)]|))) such that
A166: rng fldd = LSeg (|[(- 1),(- 3)]|,|[0,(- 3)]|) and
A167: Pldd = fldd by Th43;
A168: |[(- 1),(- 3)]| `1 = (First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))) `1 by A136, A163, Lm45, Lm58, SPPOL_1:def 3;
then LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[(- 1),(- 3)]|) is vertical by SPPOL_1:16;
then LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[(- 1),(- 3)]|) c= LSeg (|[(- 1),(- 3)]|,|[(- 1),3]|) by A133, A168, Lm25, Lm27, Lm45, GOBOARD7:63;
then A169: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[(- 1),(- 3)]|) c= rectangle ((- 1),1,(- 3),3) by Lm38, XBOOLE_1:1;
set K1 = ((((Pcm + Pml) + Plx) + Palpha) + Pnld) + Pldd;
LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[(- 1),(- 3)]|) misses C by A1, A54, A99, A120, A163, Lm84;
then A170: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[(- 1),(- 3)]|) misses Jd by A4, XBOOLE_1:7, XBOOLE_1:63;
A171: rng (((((Pcm + Pml) + Plx) + Palpha) + Pnld) + Pldd) = (((rng ((Pcm + Pml) + Plx)) \/ (rng Palpha)) \/ (rng Pnld)) \/ (rng Pldd) by Lm9;
then A172: rng PJd misses rng (((((Pcm + Pml) + Plx) + Palpha) + Pnld) + Pldd) by A124, A129, A130, A131, A132, A158, A160, A164, A165, A166, A167, A170, Lm3;
A173: LSeg (|[(- 1),(- 3)]|,|[0,(- 3)]|) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by Lm67, Lm74, XBOOLE_1:1;
LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[(- 1),(- 3)]|) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A169, Lm67, XBOOLE_1:1;
then rng (((((Pcm + Pml) + Plx) + Palpha) + Pnld) + Pldd) c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A85, A131, A132, A135, A159, A164, A165, A166, A167, A171, A173, Lm2;
then reconsider v = ((((Pcm + Pml) + Plx) + Palpha) + Pnld) + Pldd as Path of CR,DR by Th30;
consider s, t being Point of I[01] such that
A174: H . s = v . t by Lm16, Lm17, Lm21, Lm23, JGRAPH_8:6;
A175: dom H = the carrier of I[01] by FUNCT_2:def 1;
A176: dom v = the carrier of I[01] by FUNCT_2:def 1;
A177: H . s in rng PJd by A175, FUNCT_1:def 3;
v . t in rng (((((Pcm + Pml) + Plx) + Palpha) + Pnld) + Pldd) by A176, FUNCT_1:def 3;
hence contradiction by A172, A174, A177, XBOOLE_0:3; :: thesis: verum

end;

suppose A178: First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in LSeg (|[(- 1),(- 3)]|,|[0,(- 3)]|) ; :: thesis: contradiction

consider Pnd being Path of First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))),|[0,(- 3)]|, fnd being Function of I[01],((TOP-REAL 2) | (LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,(- 3)]|))) such that
A179: rng fnd = LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,(- 3)]|) and
A180: Pnd = fnd by Th43;
set K1 = (((Pcm + Pml) + Plx) + Palpha) + Pnd;
|[(- 1),(- 3)]| in LSeg (|[(- 1),(- 3)]|,|[0,(- 3)]|) by RLTOPSP1:68;
then A181: |[(- 1),(- 3)]| `2 = (First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))) `2 by A178, Lm51, SPPOL_1:def 2;
then A182: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,(- 3)]|) is horizontal by Lm23, Lm27, SPPOL_1:15;
A183: |[(- 1),(- 3)]| `1 <= (First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))) `1 by A178, Lm26, JGRAPH_6:3;
(First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))) `1 <= |[0,(- 3)]| `1 by A178, Lm22, JGRAPH_6:3;
then A184: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,(- 3)]|) c= LSeg (|[(- 1),(- 3)]|,|[0,(- 3)]|) by A181, A182, A183, Lm51, GOBOARD7:64;
then A185: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,(- 3)]|) c= rectangle ((- 1),1,(- 3),3) by Lm74, XBOOLE_1:1;
LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,(- 3)]|) misses C by A1, A184, Lm80, XBOOLE_1:63;
then A186: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,(- 3)]|) misses Jd by A4, XBOOLE_1:7, XBOOLE_1:63;
A187: rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) = ((rng ((Pcm + Pml) + Plx)) \/ (rng Palpha)) \/ (rng Pnd) by Th40;
then A188: rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) misses Jd by A124, A131, A132, A158, A179, A180, A186, XBOOLE_1:114;
LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,(- 3)]|) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A185, Lm67, XBOOLE_1:1;
then rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A85, A131, A132, A135, A159, A179, A180, A187, Lm1;
then reconsider v = (((Pcm + Pml) + Plx) + Palpha) + Pnd as Path of CR,DR by Th30;
consider s, t being Point of I[01] such that
A189: H . s = v . t by Lm16, Lm17, Lm21, Lm23, JGRAPH_8:6;
A190: dom H = the carrier of I[01] by FUNCT_2:def 1;
A191: dom v = the carrier of I[01] by FUNCT_2:def 1;
A192: H . s in rng PJd by A190, FUNCT_1:def 3;
v . t in rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) by A191, FUNCT_1:def 3;
hence contradiction by A129, A130, A188, A189, A192, XBOOLE_0:3; :: thesis: verum

end;

suppose A193: First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in LSeg (|[0,(- 3)]|,|[1,(- 3)]|) ; :: thesis: contradiction

consider Pnd being Path of First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))),|[0,(- 3)]|, fnd being Function of I[01],((TOP-REAL 2) | (LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,(- 3)]|))) such that
A194: rng fnd = LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,(- 3)]|) and
A195: Pnd = fnd by Th43;
set K1 = (((Pcm + Pml) + Plx) + Palpha) + Pnd;
|[1,(- 3)]| in LSeg (|[1,(- 3)]|,|[0,(- 3)]|) by RLTOPSP1:68;
then |[1,(- 3)]| `2 = (First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))) `2 by A193, Lm52, SPPOL_1:def 2;
then A196: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,(- 3)]|) is horizontal by Lm23, Lm31, SPPOL_1:15;
A197: |[0,(- 3)]| `2 = |[0,(- 3)]| `2 ;
A198: |[0,(- 3)]| `1 <= (First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))) `1 by A193, Lm22, JGRAPH_6:3;
(First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))) `1 <= |[1,(- 3)]| `1 by A193, Lm30, JGRAPH_6:3;
then A199: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,(- 3)]|) c= LSeg (|[1,(- 3)]|,|[0,(- 3)]|) by A196, A197, A198, Lm52, GOBOARD7:64;
then A200: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,(- 3)]|) c= rectangle ((- 1),1,(- 3),3) by Lm75, XBOOLE_1:1;
LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,(- 3)]|) misses C by A1, A199, Lm81, XBOOLE_1:63;
then A201: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,(- 3)]|) misses Jd by A4, XBOOLE_1:7, XBOOLE_1:63;
A202: rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) = ((rng ((Pcm + Pml) + Plx)) \/ (rng Palpha)) \/ (rng Pnd) by Th40;
then A203: rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) misses Jd by A124, A131, A132, A158, A194, A195, A201, XBOOLE_1:114;
LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,(- 3)]|) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A200, Lm67, XBOOLE_1:1;
then rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A85, A131, A132, A135, A159, A194, A195, A202, Lm1;
then reconsider v = (((Pcm + Pml) + Plx) + Palpha) + Pnd as Path of CR,DR by Th30;
consider s, t being Point of I[01] such that
A204: H . s = v . t by Lm16, Lm17, Lm21, Lm23, JGRAPH_8:6;
A205: dom H = the carrier of I[01] by FUNCT_2:def 1;
A206: dom v = the carrier of I[01] by FUNCT_2:def 1;
A207: H . s in rng PJd by A205, FUNCT_1:def 3;
v . t in rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) by A206, FUNCT_1:def 3;
hence contradiction by A129, A130, A203, A204, A207, XBOOLE_0:3; :: thesis: verum

end;

suppose A208: First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in LSeg (|[1,(- 3)]|,|[1,0]|) ; :: thesis: contradiction

consider Pnpd being Path of First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))),|[1,(- 3)]|, fnpd being Function of I[01],((TOP-REAL 2) | (LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[1,(- 3)]|))) such that
A209: rng fnpd = LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[1,(- 3)]|) and
A210: Pnpd = fnpd by Th43;
consider Ppdd being Path of |[1,(- 3)]|,|[0,(- 3)]|, fpdd being Function of I[01],((TOP-REAL 2) | (LSeg (|[1,(- 3)]|,|[0,(- 3)]|))) such that
A211: rng fpdd = LSeg (|[1,(- 3)]|,|[0,(- 3)]|) and
A212: Ppdd = fpdd by Th43;
A213: |[1,(- 3)]| `1 = (First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))) `1 by A137, A208, Lm46, Lm60, SPPOL_1:def 3;
then LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[1,(- 3)]|) is vertical by SPPOL_1:16;
then LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[1,(- 3)]|) c= LSeg (|[1,(- 3)]|,|[1,3]|) by A133, A213, Lm29, Lm31, Lm46, GOBOARD7:63;
then A214: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[1,(- 3)]|) c= rectangle ((- 1),1,(- 3),3) by Lm42, XBOOLE_1:1;
set K1 = ((((Pcm + Pml) + Plx) + Palpha) + Pnpd) + Ppdd;
LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[1,(- 3)]|) misses C by A1, A54, A99, A120, A208, Lm85;
then A215: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[1,(- 3)]|) misses Jd by A4, XBOOLE_1:7, XBOOLE_1:63;
A216: rng (((((Pcm + Pml) + Plx) + Palpha) + Pnpd) + Ppdd) = (((rng ((Pcm + Pml) + Plx)) \/ (rng Palpha)) \/ (rng Pnpd)) \/ (rng Ppdd) by Lm9;
then A217: rng PJd misses rng (((((Pcm + Pml) + Plx) + Palpha) + Pnpd) + Ppdd) by A124, A129, A130, A131, A132, A158, A161, A209, A210, A211, A212, A215, Lm3;
A218: LSeg (|[1,(- 3)]|,|[0,(- 3)]|) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by Lm67, Lm75, XBOOLE_1:1;
LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[1,(- 3)]|) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A214, Lm67, XBOOLE_1:1;
then rng (((((Pcm + Pml) + Plx) + Palpha) + Pnpd) + Ppdd) c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A85, A131, A132, A135, A159, A209, A210, A211, A212, A216, A218, Lm2;
then reconsider v = ((((Pcm + Pml) + Plx) + Palpha) + Pnpd) + Ppdd as Path of CR,DR by Th30;
consider s, t being Point of I[01] such that
A219: H . s = v . t by Lm16, Lm17, Lm21, Lm23, JGRAPH_8:6;
A220: dom H = the carrier of I[01] by FUNCT_2:def 1;
A221: dom v = the carrier of I[01] by FUNCT_2:def 1;
A222: H . s in rng PJd by A220, FUNCT_1:def 3;
v . t in rng (((((Pcm + Pml) + Plx) + Palpha) + Pnpd) + Ppdd) by A221, FUNCT_1:def 3;
hence contradiction by A217, A219, A222, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

suppose A223: (First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))) `2 >= 0 ; :: thesis: contradiction

per cases ( First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in LSeg (|[(- 1),0]|,|[(- 1),3]|) or First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in LSeg (|[(- 1),3]|,|[0,3]|) or First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in LSeg (|[0,3]|,|[1,3]|) or First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in LSeg (|[1,3]|,|[1,0]|) ) by A119, A223, Lm76;

suppose A224: First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in LSeg (|[(- 1),0]|,|[(- 1),3]|) ; :: thesis: contradiction

consider Pnlg being Path of First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))),|[(- 1),3]|, fnlg being Function of I[01],((TOP-REAL 2) | (LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[(- 1),3]|))) such that
A225: rng fnlg = LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[(- 1),3]|) and
A226: Pnlg = fnlg by Th43;
consider Plgc being Path of |[(- 1),3]|,|[0,3]|, flgc being Function of I[01],((TOP-REAL 2) | (LSeg (|[(- 1),3]|,|[0,3]|))) such that
A227: rng flgc = LSeg (|[(- 1),3]|,|[0,3]|) and
A228: Plgc = flgc by Th43;
A229: |[(- 1),(- 3)]| `1 = (First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))) `1 by A136, A224, Lm45, Lm57, SPPOL_1:def 3;
then LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[(- 1),3]|) is vertical by Lm24, Lm26, SPPOL_1:16;
then LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[(- 1),3]|) c= LSeg (|[(- 1),(- 3)]|,|[(- 1),3]|) by A133, A229, Lm25, Lm27, Lm45, GOBOARD7:63;
then A230: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[(- 1),3]|) c= rectangle ((- 1),1,(- 3),3) by Lm38, XBOOLE_1:1;
set K1 = ((Pdx + Palpha) + Pnlg) + Plgc;
LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[(- 1),3]|) misses C by A1, A54, A99, A120, A224, Lm82;
then A231: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[(- 1),3]|) misses Jc by A4, XBOOLE_1:7, XBOOLE_1:63;
A232: rng (((Pdx + Palpha) + Pnlg) + Plgc) = (((rng Pdx) \/ (rng Palpha)) \/ (rng Pnlg)) \/ (rng Plgc) by Lm9;
then A233: rng (((Pdx + Palpha) + Pnlg) + Plgc) misses Jc by A110, A123, A125, A126, A131, A132, A138, A225, A226, A227, A228, A231, Lm3;
A234: rng (((Pdx + Palpha) + Pnlg) + Plgc) = rng (- (((Pdx + Palpha) + Pnlg) + Plgc)) by Th32;
LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[(- 1),3]|) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A230, Lm67, XBOOLE_1:1;
then rng (((Pdx + Palpha) + Pnlg) + Plgc) c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A85, A125, A126, A131, A132, A134, A135, A139, A225, A226, A227, A228, A232, Lm2;
then reconsider v = - (((Pdx + Palpha) + Pnlg) + Plgc) as Path of CR,DR by A234, Th30;
consider s, t being Point of I[01] such that
A235: h . s = v . t by Lm16, Lm17, Lm21, Lm23, JGRAPH_8:6;
A236: dom h = the carrier of I[01] by FUNCT_2:def 1;
A237: dom v = the carrier of I[01] by FUNCT_2:def 1;
A238: h . s in rng PJc by A236, FUNCT_1:def 3;
v . t in rng (- (((Pdx + Palpha) + Pnlg) + Plgc)) by A237, FUNCT_1:def 3;
hence contradiction by A127, A128, A233, A234, A235, A238, XBOOLE_0:3; :: thesis: verum

end;

suppose A239: First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in LSeg (|[(- 1),3]|,|[0,3]|) ; :: thesis: contradiction

consider Pnc being Path of First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))),|[0,3]|, fnc being Function of I[01],((TOP-REAL 2) | (LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,3]|))) such that
A240: rng fnc = LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,3]|) and
A241: Pnc = fnc by Th43;
set K1 = (Pdx + Palpha) + Pnc;
|[(- 1),3]| in LSeg (|[(- 1),3]|,|[0,3]|) by RLTOPSP1:68;
then A242: |[(- 1),3]| `2 = (First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))) `2 by A239, Lm53, SPPOL_1:def 2;
then A243: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,3]|) is horizontal by Lm21, Lm25, SPPOL_1:15;
A244: |[(- 1),3]| `1 <= (First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))) `1 by A239, Lm24, JGRAPH_6:3;
(First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))) `1 <= |[0,3]| `1 by A239, Lm20, JGRAPH_6:3;
then A245: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,3]|) c= LSeg (|[(- 1),3]|,|[0,3]|) by A242, A243, A244, Lm53, GOBOARD7:64;
then A246: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,3]|) c= rectangle ((- 1),1,(- 3),3) by Lm70, XBOOLE_1:1;
LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,3]|) misses C by A1, A245, Lm78, XBOOLE_1:63;
then A247: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,3]|) misses Jc by A4, XBOOLE_1:7, XBOOLE_1:63;
A248: rng ((Pdx + Palpha) + Pnc) = ((rng Pdx) \/ (rng Palpha)) \/ (rng Pnc) by Th40;
then A249: rng ((Pdx + Palpha) + Pnc) misses Jc by A110, A123, A125, A126, A131, A132, A240, A241, A247, XBOOLE_1:114;
A250: rng ((Pdx + Palpha) + Pnc) = rng (- ((Pdx + Palpha) + Pnc)) by Th32;
LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,3]|) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A246, Lm67, XBOOLE_1:1;
then rng ((Pdx + Palpha) + Pnc) c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A85, A125, A126, A131, A132, A134, A135, A240, A241, A248, Lm1;
then reconsider v = - ((Pdx + Palpha) + Pnc) as Path of CR,DR by A250, Th30;
consider s, t being Point of I[01] such that
A251: h . s = v . t by Lm16, Lm17, Lm21, Lm23, JGRAPH_8:6;
A252: dom h = the carrier of I[01] by FUNCT_2:def 1;
A253: dom v = the carrier of I[01] by FUNCT_2:def 1;
A254: h . s in rng PJc by A252, FUNCT_1:def 3;
v . t in rng (- ((Pdx + Palpha) + Pnc)) by A253, FUNCT_1:def 3;
hence contradiction by A127, A128, A249, A250, A251, A254, XBOOLE_0:3; :: thesis: verum

end;

suppose A255: First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in LSeg (|[0,3]|,|[1,3]|) ; :: thesis: contradiction

consider Pnc being Path of First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))),|[0,3]|, fnc being Function of I[01],((TOP-REAL 2) | (LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,3]|))) such that
A256: rng fnc = LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,3]|) and
A257: Pnc = fnc by Th43;
set K1 = (Pdx + Palpha) + Pnc;
|[1,3]| in LSeg (|[1,3]|,|[0,3]|) by RLTOPSP1:68;
then |[1,3]| `2 = (First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))) `2 by A255, Lm54, SPPOL_1:def 2;
then A258: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,3]|) is horizontal by Lm21, Lm29, SPPOL_1:15;
A259: |[0,3]| `2 = |[0,3]| `2 ;
A260: |[0,3]| `1 <= (First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))) `1 by A255, Lm20, JGRAPH_6:3;
(First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))) `1 <= |[1,3]| `1 by A255, Lm28, JGRAPH_6:3;
then A261: LSeg (|[0,3]|,(First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))))) c= LSeg (|[0,3]|,|[1,3]|) by A258, A259, A260, Lm54, GOBOARD7:64;
then A262: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,3]|) c= rectangle ((- 1),1,(- 3),3) by Lm71, XBOOLE_1:1;
LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,3]|) misses C by A1, A261, Lm79, XBOOLE_1:63;
then A263: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,3]|) misses Jc by A4, XBOOLE_1:7, XBOOLE_1:63;
A264: rng ((Pdx + Palpha) + Pnc) = ((rng Pdx) \/ (rng Palpha)) \/ (rng Pnc) by Th40;
then A265: rng ((Pdx + Palpha) + Pnc) misses Jc by A110, A123, A125, A126, A131, A132, A256, A257, A263, XBOOLE_1:114;
A266: rng ((Pdx + Palpha) + Pnc) = rng (- ((Pdx + Palpha) + Pnc)) by Th32;
LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[0,3]|) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A262, Lm67, XBOOLE_1:1;
then rng ((Pdx + Palpha) + Pnc) c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A85, A125, A126, A131, A132, A134, A135, A256, A257, A264, Lm1;
then reconsider v = - ((Pdx + Palpha) + Pnc) as Path of CR,DR by A266, Th30;
consider s, t being Point of I[01] such that
A267: h . s = v . t by Lm16, Lm17, Lm21, Lm23, JGRAPH_8:6;
A268: dom h = the carrier of I[01] by FUNCT_2:def 1;
A269: dom v = the carrier of I[01] by FUNCT_2:def 1;
A270: h . s in rng PJc by A268, FUNCT_1:def 3;
v . t in rng (- ((Pdx + Palpha) + Pnc)) by A269, FUNCT_1:def 3;
hence contradiction by A127, A128, A265, A266, A267, A270, XBOOLE_0:3; :: thesis: verum

end;

suppose A271: First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in LSeg (|[1,3]|,|[1,0]|) ; :: thesis: contradiction

consider Pnpg being Path of First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))),|[1,3]|, fnpg being Function of I[01],((TOP-REAL 2) | (LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[1,3]|))) such that
A272: rng fnpg = LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[1,3]|) and
A273: Pnpg = fnpg by Th43;
consider Ppgc being Path of |[1,3]|,|[0,3]|, fpgc being Function of I[01],((TOP-REAL 2) | (LSeg (|[1,3]|,|[0,3]|))) such that
A274: rng fpgc = LSeg (|[1,3]|,|[0,3]|) and
A275: Ppgc = fpgc by Th43;
A276: |[1,(- 3)]| `1 = (First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))) `1 by A137, A271, Lm46, Lm59, SPPOL_1:def 3;
then LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[1,3]|) is vertical by Lm28, Lm30, SPPOL_1:16;
then LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[1,3]|) c= LSeg (|[1,(- 3)]|,|[1,3]|) by A133, A276, Lm29, Lm31, Lm46, GOBOARD7:63;
then A277: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[1,3]|) c= rectangle ((- 1),1,(- 3),3) by Lm42, XBOOLE_1:1;
set K1 = ((Pdx + Palpha) + Pnpg) + Ppgc;
LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[1,3]|) misses C by A1, A54, A99, A120, A271, Lm83;
then A278: LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[1,3]|) misses Jc by A4, XBOOLE_1:7, XBOOLE_1:63;
A279: rng (((Pdx + Palpha) + Pnpg) + Ppgc) = (((rng Pdx) \/ (rng Palpha)) \/ (rng Pnpg)) \/ (rng Ppgc) by Lm9;
then A280: rng (((Pdx + Palpha) + Pnpg) + Ppgc) misses Jc by A110, A123, A125, A126, A131, A132, A141, A272, A273, A274, A275, A278, Lm3;
A281: rng (((Pdx + Palpha) + Pnpg) + Ppgc) = rng (- (((Pdx + Palpha) + Pnpg) + Ppgc)) by Th32;
LSeg ((First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3)))),|[1,3]|) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A277, Lm67, XBOOLE_1:1;
then rng (((Pdx + Palpha) + Pnpg) + Ppgc) c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A85, A125, A126, A131, A132, A134, A135, A140, A272, A273, A274, A275, A279, Lm2;
then reconsider v = - (((Pdx + Palpha) + Pnpg) + Ppgc) as Path of CR,DR by A281, Th30;
consider s, t being Point of I[01] such that
A282: h . s = v . t by Lm16, Lm17, Lm21, Lm23, JGRAPH_8:6;
A283: dom h = the carrier of I[01] by FUNCT_2:def 1;
A284: dom v = the carrier of I[01] by FUNCT_2:def 1;
A285: h . s in rng PJc by A283, FUNCT_1:def 3;
v . t in rng (- (((Pdx + Palpha) + Pnpg) + Ppgc)) by A284, FUNCT_1:def 3;
hence contradiction by A127, A128, A280, A281, A282, A285, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

end;

end;

let V be Subset of (TOP-REAL 2); :: thesis: ( V is_inside_component_of C implies V = Ux )
assume A286: V is_inside_component_of C ; :: thesis: V = Ux
assume A287: V <> Ux ; :: thesis: contradiction
consider VP being Subset of ((TOP-REAL 2) | (C `)) such that
A288: VP = V and
A289: VP is a_component and
VP is bounded Subset of (Euclid 2) by A286, JORDAN2C:13;
reconsider T2C = (TOP-REAL 2) | (C `) as non empty SubSpace of TOP-REAL 2 ;
VP <> {} ((TOP-REAL 2) | (C `)) by A289, CONNSP_1:32;
then reconsider VP = VP as non empty Subset of T2C ;
A290: V misses C by A54, A288, SUBSET_1:23;
consider Pjd being Path of LMP C,|[0,(- 3)]|, fjd being Function of I[01],((TOP-REAL 2) | (LSeg ((LMP C),|[0,(- 3)]|))) such that
A291: rng fjd = LSeg ((LMP C),|[0,(- 3)]|) and
A292: Pjd = fjd by Th43;
consider Plk being Path of LMP Jc, UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd), flk being Function of I[01],((TOP-REAL 2) | (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))))) such that
A293: rng flk = LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) and
A294: Plk = flk by Th43;
set beta = (((Pcm + Pml) + Plk) + Pkj) + Pjd;
A295: rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) = ((((rng Pcm) \/ (rng Pml)) \/ (rng Plk)) \/ (rng Pkj)) \/ (rng Pjd) by Lm11;
dom ((((Pcm + Pml) + Plk) + Pkj) + Pjd) = [#] I[01] by FUNCT_2:def 1;
then ((((Pcm + Pml) + Plk) + Pkj) + Pjd) .: (dom ((((Pcm + Pml) + Plk) + Pkj) + Pjd)) is compact by WEIERSTR:8;
then A296: rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) is closed by RELAT_1:113;
A297: rng Pml misses V by A19, A29, A290, XBOOLE_1:1, XBOOLE_1:63;
{(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} c= LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} or x in LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) )
assume x in {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} ; :: thesis: x in LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))
then ( x = LMP Jc or x = UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) ) by TARSKI:def 2;
hence x in LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) by RLTOPSP1:68; :: thesis: verum

end;

then A298: LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) = ((LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) \ {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))}) \/ {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} by XBOOLE_1:45;
A299: (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) \ {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} misses V

proof

assume not (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) \ {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} misses V ; :: thesis: contradiction
then ex q being set st
( q in (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) \ {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} & q in V ) by XBOOLE_0:3;
then V meets Ux by A10, A83, XBOOLE_0:3;
hence contradiction by A10, A53, A287, A288, A289, CONNSP_1:35; :: thesis: verum

end;

A300: not LMP Jc in V by A17, A19, A290, XBOOLE_0:3;
not UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) in V by A18, A42, A290, XBOOLE_0:3;
then {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} misses V by A300, ZFMISC_1:51;
then A301: LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) misses V by A298, A299, XBOOLE_1:70;
A302: rng Pkj misses V by A51, A290, XBOOLE_1:63;
A303: LSeg ((LMP C),|[0,(- 3)]|) misses V by A1, A286, Th90;
LSeg (|[0,3]|,(UMP C)) misses V by A1, A286, Th89;
then ((LSeg (|[0,3]|,(UMP C))) \/ (rng Pml)) \/ (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) misses V by A297, A301, XBOOLE_1:114;
then A304: rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) misses V by A86, A87, A291, A292, A293, A294, A295, A302, A303, XBOOLE_1:114;
A305: UMP C = |[((UMP C) `1),((UMP C) `2)]| by EUCLID:53;
A306: |[0,3]| = |[(|[0,3]| `1),(|[0,3]| `2)]| by EUCLID:53;
A307: LMP C = |[((LMP C) `1),((LMP C) `2)]| by EUCLID:53;
A308: not |[(- 1),0]| in LSeg (|[0,3]|,(UMP C)) by A12, A13, A21, A23, A24, A305, A306, Lm16, JGRAPH_6:1;
not |[(- 1),0]| in rng Pml by A30, ZFMISC_1:49;
then A309: not |[(- 1),0]| in (LSeg (|[0,3]|,(UMP C))) \/ (rng Pml) by A308, XBOOLE_0:def 3;
not |[(- 1),0]| in LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) by A22, A45, A57, A58, A60, Lm16, JGRAPH_6:1;
then A310: not |[(- 1),0]| in ((LSeg (|[0,3]|,(UMP C))) \/ (rng Pml)) \/ (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) by A309, XBOOLE_0:def 3;
not |[(- 1),0]| in rng Pkj by A50, ZFMISC_1:49;
then A311: not |[(- 1),0]| in (((LSeg (|[0,3]|,(UMP C))) \/ (rng Pml)) \/ (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))))) \/ (rng Pkj) by A310, XBOOLE_0:def 3;
not |[(- 1),0]| in LSeg ((LMP C),|[0,(- 3)]|) by A34, A35, A59, A307, Lm16, Lm22, JGRAPH_6:1;
then not |[(- 1),0]| in rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A86, A87, A291, A292, A293, A294, A295, A311, XBOOLE_0:def 3;
then consider ra being positive real number such that
A312: Ball (|[(- 1),0]|,ra) misses rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A296, Th25;
A313: not |[1,0]| in LSeg (|[0,3]|,(UMP C)) by A12, A13, A21, A23, A24, A305, A306, Lm17, JGRAPH_6:1;
not |[1,0]| in rng Pml by A30, ZFMISC_1:49;
then A314: not |[1,0]| in (LSeg (|[0,3]|,(UMP C))) \/ (rng Pml) by A313, XBOOLE_0:def 3;
not |[1,0]| in LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) by A22, A45, A57, A58, A60, Lm17, JGRAPH_6:1;
then A315: not |[1,0]| in ((LSeg (|[0,3]|,(UMP C))) \/ (rng Pml)) \/ (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) by A314, XBOOLE_0:def 3;
not |[1,0]| in rng Pkj by A50, ZFMISC_1:49;
then A316: not |[1,0]| in (((LSeg (|[0,3]|,(UMP C))) \/ (rng Pml)) \/ (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))))) \/ (rng Pkj) by A315, XBOOLE_0:def 3;
not |[1,0]| in LSeg ((LMP C),|[0,(- 3)]|) by A34, A35, A59, A307, Lm17, Lm22, JGRAPH_6:1;
then not |[1,0]| in rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A86, A87, A291, A292, A293, A294, A295, A316, XBOOLE_0:def 3;
then consider rb being positive real number such that
A317: Ball (|[1,0]|,rb) misses rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A296, Th25;
set A = Ball (|[(- 1),0]|,ra);
set B = Ball (|[1,0]|,rb);
A318: |[(- 1),0]| in Ball (|[(- 1),0]|,ra) by Th16;
A319: |[1,0]| in Ball (|[1,0]|,rb) by Th16;
not VP is empty ;
then consider t being set such that
A320: t in V by A288, XBOOLE_0:def 1;
V in { W where W is Subset of (TOP-REAL 2) : W is_inside_component_of C } by A286;
then t in BDD C by A320, TARSKI:def 4;
then A321: C = Fr V by A288, A289, Lm15;
then |[(- 1),0]| in Cl V by A14, XBOOLE_0:def 4;
then Ball (|[(- 1),0]|,ra) meets V by A318, PRE_TOPC:def 7;
then consider u being set such that
A322: u in Ball (|[(- 1),0]|,ra) and
A323: u in V by XBOOLE_0:3;
|[1,0]| in Cl V by A15, A321, XBOOLE_0:def 4;
then Ball (|[1,0]|,rb) meets V by A319, PRE_TOPC:def 7;
then consider v being set such that
A324: v in Ball (|[1,0]|,rb) and
A325: v in V by XBOOLE_0:3;
reconsider u = u, v = v as Point of (TOP-REAL 2) by A322, A324;
A326: the carrier of (T2C | VP) = VP by PRE_TOPC:8;
reconsider u1 = u, v1 = v as Point of (T2C | VP) by A288, A323, A325, PRE_TOPC:8;
T2C | VP is pathwise_connected by A289, Th69;
then A327: u1,v1 are_connected by BORSUK_2:def 3;
then consider fuv being Function of I[01],(T2C | VP) such that
A328: fuv is continuous and
A329: fuv . 0 = u1 and
A330: fuv . 1 = v1 by BORSUK_2:def 1;
A331: T2C | VP = (TOP-REAL 2) | V by A288, GOBOARD9:2;
fuv is Path of u1,v1 by A327, A328, A329, A330, BORSUK_2:def 2;
then reconsider uv = fuv as Path of u,v by A327, A331, TOPALG_2:1;
A332: rng fuv c= the carrier of (T2C | VP) ;
then A333: rng uv misses rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A288, A304, A326, XBOOLE_1:63;
consider au being Path of |[(- 1),0]|,u, fau being Function of I[01],((TOP-REAL 2) | (LSeg (|[(- 1),0]|,u))) such that
A334: rng fau = LSeg (|[(- 1),0]|,u) and
A335: au = fau by Th43;
consider vb being Path of v,|[1,0]|, fvb being Function of I[01],((TOP-REAL 2) | (LSeg (v,|[1,0]|))) such that
A336: rng fvb = LSeg (v,|[1,0]|) and
A337: vb = fvb by Th43;
set AB = (au + uv) + vb;
A338: rng ((au + uv) + vb) = ((rng au) \/ (rng uv)) \/ (rng vb) by Th40;
|[(- 1),0]| in Ball (|[(- 1),0]|,ra) by Th16;
then LSeg (|[(- 1),0]|,u) c= Ball (|[(- 1),0]|,ra) by A322, JORDAN1:def 1;
then A339: LSeg (|[(- 1),0]|,u) misses rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A312, XBOOLE_1:63;
|[1,0]| in Ball (|[1,0]|,rb) by Th16;
then LSeg (v,|[1,0]|) c= Ball (|[1,0]|,rb) by A324, JORDAN1:def 1;
then LSeg (v,|[1,0]|) misses rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A317, XBOOLE_1:63;
then A340: rng ((au + uv) + vb) misses rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A333, A334, A335, A336, A337, A338, A339, XBOOLE_1:114;
A341: |[(- 1),0]|,|[1,0]| are_connected by BORSUK_2:def 3;
A342: V c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A1, A286, Th93;
then A343: LSeg (|[(- 1),0]|,u) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A11, A14, A323, JORDAN1:def 1;
A344: LSeg (v,|[1,0]|) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A11, A15, A325, A342, JORDAN1:def 1;
rng uv c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A288, A326, A332, A342, XBOOLE_1:1;
then (LSeg (|[(- 1),0]|,u)) \/ (rng uv) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A343, XBOOLE_1:8;
then rng ((au + uv) + vb) c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A85, A334, A335, A336, A337, A338, A344, XBOOLE_1:8;
then reconsider h = (au + uv) + vb as Path of AR,BR by A341, Th29;
A345: |[0,3]|,|[0,(- 3)]| are_connected by BORSUK_2:def 3;
(LSeg (|[0,3]|,(UMP C))) \/ (rng Pml) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A88, A89, XBOOLE_1:8;
then A346: ((LSeg (|[0,3]|,(UMP C))) \/ (rng Pml)) \/ (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A84, XBOOLE_1:8;
rng Pkj c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A11, A51, XBOOLE_1:1;
then A347: (((LSeg (|[0,3]|,(UMP C))) \/ (rng Pml)) \/ (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))))) \/ (rng Pkj) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A346, XBOOLE_1:8;
LSeg ((LMP C),|[0,(- 3)]|) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A11, A32, Lm63, Lm67, JORDAN1:def 1;
then rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A85, A86, A87, A291, A292, A293, A294, A295, A347, XBOOLE_1:8;
then reconsider v = (((Pcm + Pml) + Plk) + Pkj) + Pjd as Path of CR,DR by A345, Th29;
consider s, t being Point of I[01] such that
A348: h . s = v . t by Lm16, Lm17, Lm21, Lm23, JGRAPH_8:6;
A349: dom h = the carrier of I[01] by FUNCT_2:def 1;
A350: dom v = the carrier of I[01] by FUNCT_2:def 1;
A351: h . s in rng ((au + uv) + vb) by A349, FUNCT_1:def 3;
v . t in rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A350, FUNCT_1:def 3;
hence contradiction by A340, A348, A351, XBOOLE_0:3; :: thesis: verum