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:43;
A17: LMP Jc in Jc by JORDAN21:44;
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:43;
A22: (LMP Jc) `1 = 0 by A8, A9, A12, A13, EUCLID:56;
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:56;
A25: UMP C <> |[(- 1),0 ]| by A12, A13, Lm16, EUCLID:56;
A26: UMP C <> |[1,0 ]| by A12, A13, Lm17, EUCLID:56;
A27: LMP Jc <> |[(- 1),0 ]| by A8, A9, A12, A13, Lm16, EUCLID:56;
A28: LMP Jc <> |[1,0 ]| by A8, A9, A12, A13, Lm17, EUCLID:56;
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:37;
A34: |[0 ,(- 3)]| `2 <= (LMP C) `2 by A1, A7, A18, Lm23, Th84;
A35: (LMP C) `1 = 0 by A12, A13, EUCLID:56;
LMP Jc in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A12, A13, A22, JORDAN6:34;
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:42;
then LMP C in LSeg (LMP Jc),|[0 ,(- 3)]| by A22, A34, A35, Lm22, GOBOARD7:8;
then A37: not (LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd is empty by A7, XBOOLE_0:def 4;
A38: (LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd is compact by COMPTS_1:20;
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, A38, JORDAN21:43;
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:69;
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:56;
A47: UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) <> |[1,0 ]| by A45, EUCLID:56;
A48: LMP C <> |[(- 1),0 ]| by A35, EUCLID:56;
LMP C <> |[1,0 ]| by A35, EUCLID:56;
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:70;
A53: Component_of (Down ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))),(C ` )) is a_component by CONNSP_1:43;
A54: the carrier of ((TOP-REAL 2) | (C ` )) = C ` by PRE_TOPC:29;
A55: LSeg (LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) is vertical by A22, A45, SPPOL_1:37;
A56: UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) in LSeg (LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) by RLTOPSP1:69;
A57: LMP Jc = |[((LMP Jc) `1 ),((LMP Jc) `2 )]| by EUCLID:57;
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:57;
A59: |[0 ,(- 3)]| = |[(|[0 ,(- 3)]| `1 ),(|[0 ,(- 3)]| `2 )]| by EUCLID:57;
|[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:9;
A61: |[(- 1),0 ]| <> UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) by A45, EUCLID:56;
|[1,0 ]| <> UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) by A45, EUCLID:56;
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:11;
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:34;
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:42;
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:65;
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:50;
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:34;

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:42;
q `2 <= (LMP Jc) `2 by A22, A45, A57, A58, A60, A68, JGRAPH_6:9;
then (LMP Jc) `2 = q `2 by A72, XXREAL_0:1;
then LMP Jc = q by A12, A13, A22, A70, TOPREAL3:11;
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:132, XBOOLE_1:17;
A76: E-bound ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) <= E-bound (LSeg (LMP Jc),|[0 ,(- 3)]|) by A73, PSCOMP_1:130, XBOOLE_1:17;
A77: W-bound ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) = E-bound ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) by A37, A38, A39, SPRECT_1:17;
A78: W-bound (LSeg (LMP Jc),|[0 ,(- 3)]|) = |[0 ,(- 3)]| `1 by A22, Lm22, SPRECT_1:62;
then W-bound (LSeg (LMP Jc),|[0 ,(- 3)]|) = W-bound ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) by A22, A75, A76, A77, Lm22, SPRECT_1:65;
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:34;
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 A38, JORDAN21:41;
(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) `2 <= q `2 by A22, A45, A57, A58, A60, A68, JGRAPH_6:9;
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:11;
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:29;

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:52;
then X is connected by CONNSP_1:24;
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:38;
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:29;
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:29;
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 3 :: 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:16;
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:18;
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:24;
(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:30;
A98: P1 is_an_arc_of (1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc)),u by A96, TOPREAL4:3;
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:43;
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:9
.= (1 / 2) * (((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) `1 ) + ((LMP Jc) `1 )) by TOPREAL3:7
.= 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:37;
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:57;
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:65;
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:9;
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:34;
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:42; :: 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:4;
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:4;
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:23, JORDAN6:11;
P1 is closed by A96, JORDAN6:12, TOPREAL4:3;
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:41;
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:39, TOPREAL4:3;
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:5, 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:5, 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:3;
A136: |[(- 1),(- 3)]| in LSeg |[(- 1),(- 3)]|,|[(- 1),3]| by RLTOPSP1:69;
A137: |[1,(- 3)]| in LSeg |[1,(- 3)]|,|[1,3]| by RLTOPSP1:69;
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:37;
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:65;
LMP Jc in LSeg (LMP Jc),((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))) by RLTOPSP1:69;
then {(LMP Jc)} c= LSeg (LMP Jc),((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))) by ZFMISC_1:37;
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:64;
A156: q <> LMP Jc by A154, ZFMISC_1:64;
q <> UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) by A22, A57, A103, A105, A106, A107, A155, JGRAPH_6:9;
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:43;
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:56;
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:37;
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:65;
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 5;
v . t in rng (((((Pcm + Pml) + Plx) + Palpha) + Pnld) + Pldd) by A176, FUNCT_1:def 5;
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:69;
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:36;
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:11;
(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:11;
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:66;
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 5;
v . t in rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) by A191, FUNCT_1:def 5;
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:69;
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:36;
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:11;
(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:11;
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:66;
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 5;
v . t in rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) by A206, FUNCT_1:def 5;
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:37;
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:65;
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 5;
v . t in rng (((((Pcm + Pml) + Plx) + Palpha) + Pnpd) + Ppdd) by A221, FUNCT_1:def 5;
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:37;
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:65;
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 5;
v . t in rng (- (((Pdx + Palpha) + Pnlg) + Plgc)) by A237, FUNCT_1:def 5;
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:69;
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:36;
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:11;
(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:11;
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:66;
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 5;
v . t in rng (- ((Pdx + Palpha) + Pnc)) by A253, FUNCT_1:def 5;
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:69;
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:36;
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:11;
(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:11;
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:66;
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 5;
v . t in rng (- ((Pdx + Palpha) + Pnc)) by A269, FUNCT_1:def 5;
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:37;
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:65;
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 5;
v . t in rng (- (((Pdx + Palpha) + Pnpg) + Ppgc)) by A284, FUNCT_1:def 5;
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:17;
reconsider T2C = (TOP-REAL 2) | (C ` ) as non empty SubSpace of TOP-REAL 2 ;
VP <> {} ((TOP-REAL 2) | (C ` )) by A289, CONNSP_1:34;
then reconsider VP = VP as non empty Subset of T2C ;
A290: V misses C by A54, A288, SUBSET_1:43;
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:14;
then A296: rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) is closed by RELAT_1:146;
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:69; :: 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:37; :: 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:57;
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:57;
A306: |[0 ,3]| = |[(|[0 ,3]| `1 ),(|[0 ,3]| `2 )]| by EUCLID:57;
A307: LMP C = |[((LMP C) `1 ),((LMP C) `2 )]| by EUCLID:57;
A308: not |[(- 1),0 ]| in LSeg |[0 ,3]|,(UMP C) by A12, A13, A21, A23, A24, A305, A306, Lm16, JGRAPH_6:9;
not |[(- 1),0 ]| in rng Pml by A30, ZFMISC_1:55;
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:9;
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:55;
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:9;
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:9;
not |[1,0 ]| in rng Pml by A30, ZFMISC_1:55;
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:9;
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:55;
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:9;
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 13;
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 13;
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:29;
reconsider u1 = u, v1 = v as Point of (T2C | VP) by A288, A323, A325, PRE_TOPC:29;
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:4;
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 5;
v . t in rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A350, FUNCT_1:def 5;
hence contradiction by A340, A348, A351, XBOOLE_0:3; :: thesis: verum