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;
A15: |[1,0]| in C by A1;
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;
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;
A38: (LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd is vertical by A33, Th4;
then A39: UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) in (LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd by A37, JORDAN21:30;
then A40: UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) in LSeg ((LMP Jc),|[0,(- 3)]|) by XBOOLE_0:def 4;
A41: UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) in Jd by A39, XBOOLE_0:def 4;
then A42: UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) in C by A18;
A43: |[0,(- 3)]| in LSeg ((LMP Jc),|[0,(- 3)]|) by RLTOPSP1:68;
then A44: (UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `1 = 0 by A33, A40, Lm22;
then A45: UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) <> |[(- 1),0]| by EUCLID:52;
A46: UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) <> |[1,0]| by A44, EUCLID:52;
A47: 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
A48: rng Pkj c= Jd and
A49: rng Pkj misses {|[(- 1),0]|,|[1,0]|} by A3, A7, A41, A45, A46, A47, Th44;
set kj = rng Pkj;
A50: rng Pkj c= C by A18, A48;
A51: (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;
A52: Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) is a_component by CONNSP_1:40;
A53: the carrier of ((TOP-REAL 2) | (C `)) = C ` by PRE_TOPC:8;
A54: LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) is vertical by A22, A44, SPPOL_1:16;
A55: UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) in LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) by RLTOPSP1:68;
A56: LMP Jc = |[((LMP Jc) `1),((LMP Jc) `2)]| by EUCLID:53;
A57: 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;
A58: |[0,(- 3)]| = |[(|[0,(- 3)]| `1),(|[0,(- 3)]| `2)]| by EUCLID:53;
|[0,(- 3)]| `2 <= (LMP Jc) `2 by A1, A17, A19, Lm23, Th84;
then A59: (UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `2 <= (LMP Jc) `2 by A22, A40, A56, A58, Lm22, JGRAPH_6:1;
A60: |[(- 1),0]| <> UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) by A44, EUCLID:52;
|[1,0]| <> UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) by A44, EUCLID:52;
then not UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) in {|[(- 1),0]|,|[1,0]|} by A60, TARSKI:def 2;
then A61: UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) <> LMP Jc by A5, A17, A41, XBOOLE_0:def 4;
then (UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `2 <> (LMP Jc) `2 by A22, A44, TOPREAL3:6;
then A62: (UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `2 < (LMP Jc) `2 by A59, XXREAL_0:1;
UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A12, A13, A44, JORDAN6:31;
then UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) by A18, A41, 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 A63: LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) c= LSeg ((LMP Jc),|[0,(- 3)]|) by A33, A44, A54, A59, Lm22, GOBOARD7:63;
A64: (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 object ; :: 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
A65: q in (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) \ {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} and
A66: not q in C ` ; :: thesis: contradiction
A67: q in LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) by A65, XBOOLE_0:def 5;
reconsider q = q as Point of (TOP-REAL 2) by A65;
A68: q in C by A66, SUBSET_1:29;
A69: q `1 = ((W-bound C) + (E-bound C)) / 2 by A12, A13, A44, A54, A55, A67;
then A70: 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, A68, XBOOLE_0:def 3;
suppose q in Jd ; :: thesis: contradiction
then A72: q in (LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd by A63, A67, XBOOLE_0:def 4;
A73: q `1 = |[0,(- 3)]| `1 by A33, A43, A63, A67;
A74: W-bound (LSeg ((LMP Jc),|[0,(- 3)]|)) <= W-bound ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) by A72, PSCOMP_1:69, XBOOLE_1:17;
A75: E-bound ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) <= E-bound (LSeg ((LMP Jc),|[0,(- 3)]|)) by A72, PSCOMP_1:67, XBOOLE_1:17;
A76: W-bound ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) = E-bound ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) by A37, A38, SPRECT_1:15;
A77: 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, A74, A75, A76, 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 A73, A76, A77, 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 A72, XBOOLE_0:def 4;
then A78: 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, A44, A56, A57, A59, A67, JGRAPH_6:1;
then (UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `2 = q `2 by A78, XXREAL_0:1;
then UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) = q by A12, A13, A44, A69, TOPREAL3:6;
then q in {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} by TARSKI:def 2;
hence contradiction by A65, 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 :: thesis: not (1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)) in {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))}
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 A61, Th1; :: thesis: verum
end;
then A79: (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 A51, 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 A64, CONNSP_3:27;
then A80: (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 A64, A79, CONNSP_3:26;
then A81: X meets Ux by A10, A79, XBOOLE_0:3;
(LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) \ {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} is convex by JORDAN1:46;
then X is connected by CONNSP_1:23;
then A82: X c= Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) by A10, A52, A81, CONNSP_1:36;
A83: LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A11, A20, A42, JORDAN1:def 1;
A84: 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
A85: rng fcm = LSeg (|[0,3]|,(UMP C)) and
A86: Pcm = fcm by Th43;
A87: LSeg (|[0,3]|,(UMP C)) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A11, A16, Lm62, Lm67, JORDAN1:def 1;
A88: rng Pml c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A11, A31;
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 A89: Ux is_a_component_of C ` by A10, A52; :: 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 RLTOPSP1:42;
then consider u being object such that
A90: u in Ux and
A91: not u in Ball (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),10) ;
A92: closed_inside_of_rectangle ((- 1),1,(- 3),3) c= Ball (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),10) by A51, A83, Lm89;
reconsider u = u as Point of (TOP-REAL 2) by A90;
A93: Ux is open by A89, SPRECT_3:8;
Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) is connected by A52;
then A94: 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
A95: P1 is_S-P_arc_joining (1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)),u and
A96: P1 c= Ux by A10, A80, A90, A91, A93, A94, TOPREAL4:29;
A97: P1 is_an_arc_of (1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)),u by A95, TOPREAL4:2;
reconsider P2 = P1 as Subset of ((TOP-REAL 2) | (C `)) by A10, A96, XBOOLE_1:1;
A98: P2 c= Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) by A10, A96;
A99: P2 misses C by A53, SUBSET_1:23;
then A100: P2 misses Jc by A4, XBOOLE_1:7, XBOOLE_1:63;
A101: P2 misses Jd by A4, A99, XBOOLE_1:7, XBOOLE_1:63;
A102: ((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, A44 ;
then A103: LSeg (|[0,(- 3)]|,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) is vertical by Lm22, SPPOL_1:16;
A104: (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;
A105: ((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))) `2 < (LMP Jc) `2 by A62, Th3;
A106: (UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `2 < ((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))) `2 by A62, Th2;
then A107: |[0,(- 3)]| `2 <= ((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))) `2 by A1, A18, A41, Lm23, Th84, XXREAL_0:2;
|[0,(- 3)]| `1 = |[0,(- 3)]| `1 ;
then A108: LSeg (|[0,(- 3)]|,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) c= LSeg (|[0,(- 3)]|,(LMP Jc)) by A33, A103, A105, A107, GOBOARD7:63;
A109: 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 object such that
A110: q in LSeg (|[0,(- 3)]|,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) and
A111: q in Jc by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A110;
q `2 <= ((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))) `2 by A58, A102, A104, A107, A110, Lm22, JGRAPH_6:1;
then A112: q `2 < (LMP Jc) `2 by A105, XXREAL_0:2;
q `1 = 0 by A33, A43, A108, A110, Lm22;
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 A111, XBOOLE_0:def 4;
hence contradiction by A8, A9, A112, 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)));
A113: not u in closed_inside_of_rectangle ((- 1),1,(- 3),3) by A91, A92;
A114: Fr (closed_inside_of_rectangle ((- 1),1,(- 3),3)) = rectangle ((- 1),1,(- 3),3) by Th52;
u in P1 by A97, TOPREAL1:1;
then A115: P1 \ (closed_inside_of_rectangle ((- 1),1,(- 3),3)) <> {} (TOP-REAL 2) by A113, XBOOLE_0:def 5;
(1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)) in P1 by A97, TOPREAL1:1;
then P1 meets closed_inside_of_rectangle ((- 1),1,(- 3),3) by A51, A83, XBOOLE_0:3;
then A116: P1 meets rectangle ((- 1),1,(- 3),3) by A97, A114, A115, CONNSP_1:22, JORDAN6:10;
P1 is closed by A95, JORDAN6:11, TOPREAL4:2;
then A117: 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 A97, A116, JORDAN5C:def 1;
then A118: 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;
A119: First_Point (P1,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),u,(rectangle ((- 1),1,(- 3),3))) in P1 by A117, 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)))));
A120: - 3 < (UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) `2 by A1, A18, A41, 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 A105, XXREAL_0:2;
then not (1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)) in rectangle ((- 1),1,(- 3),3) by A21, A102, A104, A106, A120, Lm86;
then A121: 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 A95, A118, A119, JORDAN16:24, TOPREAL4:2;
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))))) misses Jc by A100, JORDAN16:2, XBOOLE_1:63;
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 Jd by A101, 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
A124: rng fdx = LSeg (|[0,(- 3)]|,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) and
A125: 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
A126: rng fJc = Jc and
A127: 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
A128: rng fJd = Jd and
A129: 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
A130: 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
A131: Palpha = falpha by A121, 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 A118, Lm67;
then A132: 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, A84, A126, A127;
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, A84, A128, A129;
then reconsider H = PJd as Path of AR,BR by Th30;
A133: LSeg (|[0,(- 3)]|,((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A51, A83, Lm63, Lm67, JORDAN1:def 1;
A134: 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 A51, A83, A95, A113, Th57, TOPREAL4:2;
A135: |[(- 1),(- 3)]| in LSeg (|[(- 1),(- 3)]|,|[(- 1),3]|) by RLTOPSP1:68;
A136: |[1,(- 3)]| in LSeg (|[1,(- 3)]|,|[1,3]|) by RLTOPSP1:68;
LSeg (|[(- 1),3]|,|[0,3]|) misses C by A1, Lm78;
then A137: LSeg (|[(- 1),3]|,|[0,3]|) misses Jc by A4, XBOOLE_1:7, XBOOLE_1:63;
A138: LSeg (|[(- 1),3]|,|[0,3]|) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by Lm67, Lm70;
A139: LSeg (|[1,3]|,|[0,3]|) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by Lm67, Lm71;
LSeg (|[1,3]|,|[0,3]|) misses C by A1, Lm79;
then A140: 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
A141: rng flx = LSeg ((LMP Jc),((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) and
A142: Plx = flx by Th43;
set PCX = (Pcm + Pml) + Plx;
A143: rng ((Pcm + Pml) + Plx) = ((rng Pcm) \/ (rng Pml)) \/ (rng Plx) by Th40;
A144: rng Pml misses Jd
proof
assume rng Pml meets Jd ; :: thesis: contradiction
then consider q being object such that
A145: q in rng Pml and
A146: q in Jd by XBOOLE_0:3;
q in {|[(- 1),0]|,|[1,0]|} by A5, A29, A145, A146, XBOOLE_0:def 4;
hence contradiction by A30, A145, XBOOLE_0:3; :: thesis: verum
end;
A147: (LSeg (|[0,3]|,(UMP C))) /\ C = {(UMP C)} by A1, Th91;
A148: LSeg (|[0,3]|,(UMP C)) misses Jd
proof
assume LSeg (|[0,3]|,(UMP C)) meets Jd ; :: thesis: contradiction
then consider q being object such that
A149: q in LSeg (|[0,3]|,(UMP C)) and
A150: q in Jd by XBOOLE_0:3;
q in {(UMP C)} by A18, A147, A149, A150, XBOOLE_0:def 4;
then q = UMP C by TARSKI:def 1;
then UMP C in {|[(- 1),0]|,|[1,0]|} by A5, A6, A150, 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, A102, SPPOL_1:16;
then A151: 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 A44, A54, A102, A105, A106, 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 A152: 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 object ; :: 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 A153: 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 A154: q in LSeg ((LMP Jc),((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc)))) by ZFMISC_1:56;
A155: q <> LMP Jc by A153, ZFMISC_1:56;
q <> UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) by A22, A56, A102, A104, A105, A106, A154, JGRAPH_6:1;
then not q in {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} by A155, 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 A151, A154, 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 A64;
then (LSeg ((LMP Jc),((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))))) \ {(LMP Jc)} misses C by SUBSET_1:23;
then A156: (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 A152, A156, XBOOLE_1:70;
then A157: rng ((Pcm + Pml) + Plx) misses Jd by A85, A86, A141, A142, A143, A144, A148, 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 A83, A151;
then A158: rng ((Pcm + Pml) + Plx) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A85, A86, A87, A88, A141, A142, A143, Lm1;
LSeg (|[(- 1),(- 3)]|,|[0,(- 3)]|) misses C by A1, Lm80;
then A159: 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 A160: 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 A161: (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 A118, A161, Lm77;
suppose A162: 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
A163: 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
A164: 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
A165: rng fldd = LSeg (|[(- 1),(- 3)]|,|[0,(- 3)]|) and
A166: Pldd = fldd by Th43;
A167: |[(- 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 A135, A162, Lm45, Lm58;
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 A132, A167, Lm25, Lm27, Lm45, GOBOARD7:63;
then A168: 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;
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, A53, A98, A119, A162, Lm84;
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)]|) misses Jd by A4, XBOOLE_1:7, XBOOLE_1:63;
A170: rng (((((Pcm + Pml) + Plx) + Palpha) + Pnld) + Pldd) = (((rng ((Pcm + Pml) + Plx)) \/ (rng Palpha)) \/ (rng Pnld)) \/ (rng Pldd) by Lm9;
then A171: rng PJd misses rng (((((Pcm + Pml) + Plx) + Palpha) + Pnld) + Pldd) by A123, A128, A129, A130, A131, A157, A159, A163, A164, A165, A166, A169, Lm3;
A172: LSeg (|[(- 1),(- 3)]|,|[0,(- 3)]|) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by Lm67, Lm74;
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 A168, Lm67;
then rng (((((Pcm + Pml) + Plx) + Palpha) + Pnld) + Pldd) c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A84, A130, A131, A134, A158, A163, A164, A165, A166, A170, A172, 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
A173: H . s = v . t by Lm16, Lm17, Lm21, Lm23, JGRAPH_8:6;
A174: dom H = the carrier of I[01] by FUNCT_2:def 1;
A175: dom v = the carrier of I[01] by FUNCT_2:def 1;
A176: H . s in rng PJd by A174, FUNCT_1:def 3;
v . t in rng (((((Pcm + Pml) + Plx) + Palpha) + Pnld) + Pldd) by A175, FUNCT_1:def 3;
hence contradiction by A171, A173, A176, XBOOLE_0:3; :: thesis: verum
end;
suppose A177: 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
A178: 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
A179: Pnd = fnd by Th43;
set K1 = (((Pcm + Pml) + Plx) + Palpha) + Pnd;
|[(- 1),(- 3)]| in LSeg (|[(- 1),(- 3)]|,|[0,(- 3)]|) by RLTOPSP1:68;
then A180: |[(- 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 A177, Lm51;
then A181: 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;
A182: |[(- 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 A177, 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 A177, Lm22, JGRAPH_6:3;
then A183: 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 A180, A181, A182, Lm51, GOBOARD7:64;
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= rectangle ((- 1),1,(- 3),3) by Lm74;
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, A183, Lm80, XBOOLE_1:63;
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)]|) misses Jd by A4, XBOOLE_1:7, XBOOLE_1:63;
A186: rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) = ((rng ((Pcm + Pml) + Plx)) \/ (rng Palpha)) \/ (rng Pnd) by Th40;
then A187: rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) misses Jd by A123, A130, A131, A157, A178, A179, A185, 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 A184, Lm67;
then rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A84, A130, A131, A134, A158, A178, A179, A186, 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
A188: H . s = v . t by Lm16, Lm17, Lm21, Lm23, JGRAPH_8:6;
A189: dom H = the carrier of I[01] by FUNCT_2:def 1;
A190: dom v = the carrier of I[01] by FUNCT_2:def 1;
A191: H . s in rng PJd by A189, FUNCT_1:def 3;
v . t in rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) by A190, FUNCT_1:def 3;
hence contradiction by A128, A129, A187, A188, A191, XBOOLE_0:3; :: thesis: verum
end;
suppose A192: 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
A193: 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
A194: 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 A192, Lm52;
then A195: 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;
A196: |[0,(- 3)]| `2 = |[0,(- 3)]| `2 ;
A197: |[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 A192, 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 A192, Lm30, JGRAPH_6:3;
then A198: 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 A195, A196, A197, Lm52, GOBOARD7:64;
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= rectangle ((- 1),1,(- 3),3) by Lm75;
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, A198, Lm81, XBOOLE_1:63;
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)]|) misses Jd by A4, XBOOLE_1:7, XBOOLE_1:63;
A201: rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) = ((rng ((Pcm + Pml) + Plx)) \/ (rng Palpha)) \/ (rng Pnd) by Th40;
then A202: rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) misses Jd by A123, A130, A131, A157, A193, A194, A200, 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 A199, Lm67;
then rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A84, A130, A131, A134, A158, A193, A194, A201, 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
A203: H . s = v . t by Lm16, Lm17, Lm21, Lm23, JGRAPH_8:6;
A204: dom H = the carrier of I[01] by FUNCT_2:def 1;
A205: dom v = the carrier of I[01] by FUNCT_2:def 1;
A206: H . s in rng PJd by A204, FUNCT_1:def 3;
v . t in rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) by A205, FUNCT_1:def 3;
hence contradiction by A128, A129, A202, A203, A206, XBOOLE_0:3; :: thesis: verum
end;
suppose A207: 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
A208: 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
A209: 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
A210: rng fpdd = LSeg (|[1,(- 3)]|,|[0,(- 3)]|) and
A211: Ppdd = fpdd by Th43;
A212: |[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, A207, Lm46, Lm60;
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 A132, A212, Lm29, Lm31, Lm46, GOBOARD7:63;
then A213: 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;
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, A53, A98, A119, A207, Lm85;
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)]|) misses Jd by A4, XBOOLE_1:7, XBOOLE_1:63;
A215: rng (((((Pcm + Pml) + Plx) + Palpha) + Pnpd) + Ppdd) = (((rng ((Pcm + Pml) + Plx)) \/ (rng Palpha)) \/ (rng Pnpd)) \/ (rng Ppdd) by Lm9;
then A216: rng PJd misses rng (((((Pcm + Pml) + Plx) + Palpha) + Pnpd) + Ppdd) by A123, A128, A129, A130, A131, A157, A160, A208, A209, A210, A211, A214, Lm3;
A217: LSeg (|[1,(- 3)]|,|[0,(- 3)]|) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by Lm67, Lm75;
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 A213, Lm67;
then rng (((((Pcm + Pml) + Plx) + Palpha) + Pnpd) + Ppdd) c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A84, A130, A131, A134, A158, A208, A209, A210, A211, A215, A217, 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
A218: H . s = v . t by Lm16, Lm17, Lm21, Lm23, JGRAPH_8:6;
A219: dom H = the carrier of I[01] by FUNCT_2:def 1;
A220: dom v = the carrier of I[01] by FUNCT_2:def 1;
A221: H . s in rng PJd by A219, FUNCT_1:def 3;
v . t in rng (((((Pcm + Pml) + Plx) + Palpha) + Pnpd) + Ppdd) by A220, FUNCT_1:def 3;
hence contradiction by A216, A218, A221, XBOOLE_0:3; :: thesis: verum
end;
end;
end;
suppose A222: (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 A118, A222, Lm76;
suppose A223: 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
A224: 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
A225: 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
A226: rng flgc = LSeg (|[(- 1),3]|,|[0,3]|) and
A227: Plgc = flgc by Th43;
A228: |[(- 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 A135, A223, Lm45, Lm57;
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 A132, A228, Lm25, Lm27, Lm45, GOBOARD7:63;
then A229: 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;
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, A53, A98, A119, A223, Lm82;
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]|) misses Jc by A4, XBOOLE_1:7, XBOOLE_1:63;
A231: rng (((Pdx + Palpha) + Pnlg) + Plgc) = (((rng Pdx) \/ (rng Palpha)) \/ (rng Pnlg)) \/ (rng Plgc) by Lm9;
then A232: rng (((Pdx + Palpha) + Pnlg) + Plgc) misses Jc by A109, A122, A124, A125, A130, A131, A137, A224, A225, A226, A227, A230, Lm3;
A233: 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 A229, Lm67;
then rng (((Pdx + Palpha) + Pnlg) + Plgc) c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A84, A124, A125, A130, A131, A133, A134, A138, A224, A225, A226, A227, A231, Lm2;
then reconsider v = - (((Pdx + Palpha) + Pnlg) + Plgc) as Path of CR,DR by A233, Th30;
consider s, t being Point of I[01] such that
A234: h . s = v . t by Lm16, Lm17, Lm21, Lm23, JGRAPH_8:6;
A235: dom h = the carrier of I[01] by FUNCT_2:def 1;
A236: dom v = the carrier of I[01] by FUNCT_2:def 1;
A237: h . s in rng PJc by A235, FUNCT_1:def 3;
v . t in rng (- (((Pdx + Palpha) + Pnlg) + Plgc)) by A236, FUNCT_1:def 3;
hence contradiction by A126, A127, A232, A233, A234, A237, XBOOLE_0:3; :: thesis: verum
end;
suppose A238: 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
A239: 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
A240: Pnc = fnc by Th43;
set K1 = (Pdx + Palpha) + Pnc;
|[(- 1),3]| in LSeg (|[(- 1),3]|,|[0,3]|) by RLTOPSP1:68;
then A241: |[(- 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 A238, Lm53;
then A242: 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;
A243: |[(- 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 A238, 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 A238, Lm20, JGRAPH_6:3;
then A244: 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 A241, A242, A243, Lm53, GOBOARD7:64;
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= rectangle ((- 1),1,(- 3),3) by Lm70;
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, A244, Lm78, XBOOLE_1:63;
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]|) misses Jc by A4, XBOOLE_1:7, XBOOLE_1:63;
A247: rng ((Pdx + Palpha) + Pnc) = ((rng Pdx) \/ (rng Palpha)) \/ (rng Pnc) by Th40;
then A248: rng ((Pdx + Palpha) + Pnc) misses Jc by A109, A122, A124, A125, A130, A131, A239, A240, A246, XBOOLE_1:114;
A249: 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 A245, Lm67;
then rng ((Pdx + Palpha) + Pnc) c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A84, A124, A125, A130, A131, A133, A134, A239, A240, A247, Lm1;
then reconsider v = - ((Pdx + Palpha) + Pnc) as Path of CR,DR by A249, Th30;
consider s, t being Point of I[01] such that
A250: h . s = v . t by Lm16, Lm17, Lm21, Lm23, JGRAPH_8:6;
A251: dom h = the carrier of I[01] by FUNCT_2:def 1;
A252: dom v = the carrier of I[01] by FUNCT_2:def 1;
A253: h . s in rng PJc by A251, FUNCT_1:def 3;
v . t in rng (- ((Pdx + Palpha) + Pnc)) by A252, FUNCT_1:def 3;
hence contradiction by A126, A127, A248, A249, A250, A253, XBOOLE_0:3; :: thesis: verum
end;
suppose A254: 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
A255: 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
A256: 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 A254, Lm54;
then A257: 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;
A258: |[0,3]| `2 = |[0,3]| `2 ;
A259: |[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 A254, 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 A254, Lm28, JGRAPH_6:3;
then A260: 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 A257, A258, A259, Lm54, GOBOARD7:64;
then A261: 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;
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, A260, Lm79, XBOOLE_1:63;
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]|) misses Jc by A4, XBOOLE_1:7, XBOOLE_1:63;
A263: rng ((Pdx + Palpha) + Pnc) = ((rng Pdx) \/ (rng Palpha)) \/ (rng Pnc) by Th40;
then A264: rng ((Pdx + Palpha) + Pnc) misses Jc by A109, A122, A124, A125, A130, A131, A255, A256, A262, XBOOLE_1:114;
A265: 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 A261, Lm67;
then rng ((Pdx + Palpha) + Pnc) c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A84, A124, A125, A130, A131, A133, A134, A255, A256, A263, Lm1;
then reconsider v = - ((Pdx + Palpha) + Pnc) as Path of CR,DR by A265, Th30;
consider s, t being Point of I[01] such that
A266: h . s = v . t by Lm16, Lm17, Lm21, Lm23, JGRAPH_8:6;
A267: dom h = the carrier of I[01] by FUNCT_2:def 1;
A268: dom v = the carrier of I[01] by FUNCT_2:def 1;
A269: h . s in rng PJc by A267, FUNCT_1:def 3;
v . t in rng (- ((Pdx + Palpha) + Pnc)) by A268, FUNCT_1:def 3;
hence contradiction by A126, A127, A264, A265, A266, A269, XBOOLE_0:3; :: thesis: verum
end;
suppose A270: 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
A271: 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
A272: 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
A273: rng fpgc = LSeg (|[1,3]|,|[0,3]|) and
A274: Ppgc = fpgc by Th43;
A275: |[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, A270, Lm46, Lm59;
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 A132, A275, Lm29, Lm31, Lm46, GOBOARD7:63;
then A276: 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;
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, A53, A98, A119, A270, Lm83;
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]|) misses Jc by A4, XBOOLE_1:7, XBOOLE_1:63;
A278: rng (((Pdx + Palpha) + Pnpg) + Ppgc) = (((rng Pdx) \/ (rng Palpha)) \/ (rng Pnpg)) \/ (rng Ppgc) by Lm9;
then A279: rng (((Pdx + Palpha) + Pnpg) + Ppgc) misses Jc by A109, A122, A124, A125, A130, A131, A140, A271, A272, A273, A274, A277, Lm3;
A280: 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 A276, Lm67;
then rng (((Pdx + Palpha) + Pnpg) + Ppgc) c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A84, A124, A125, A130, A131, A133, A134, A139, A271, A272, A273, A274, A278, Lm2;
then reconsider v = - (((Pdx + Palpha) + Pnpg) + Ppgc) as Path of CR,DR by A280, Th30;
consider s, t being Point of I[01] such that
A281: h . s = v . t by Lm16, Lm17, Lm21, Lm23, JGRAPH_8:6;
A282: dom h = the carrier of I[01] by FUNCT_2:def 1;
A283: dom v = the carrier of I[01] by FUNCT_2:def 1;
A284: h . s in rng PJc by A282, FUNCT_1:def 3;
v . t in rng (- (((Pdx + Palpha) + Pnpg) + Ppgc)) by A283, FUNCT_1:def 3;
hence contradiction by A126, A127, A279, A280, A281, A284, 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 A285: V is_inside_component_of C ; :: thesis: V = Ux
assume A286: V <> Ux ; :: thesis: contradiction
consider VP being Subset of ((TOP-REAL 2) | (C `)) such that
A287: VP = V and
A288: VP is a_component and
VP is bounded Subset of (Euclid 2) by A285, JORDAN2C:13;
reconsider T2C = (TOP-REAL 2) | (C `) as non empty SubSpace of TOP-REAL 2 ;
VP <> {} ((TOP-REAL 2) | (C `)) by A288, CONNSP_1:32;
then reconsider VP = VP as non empty Subset of T2C ;
A289: V misses C by A53, A287, 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
A290: rng fjd = LSeg ((LMP C),|[0,(- 3)]|) and
A291: 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
A292: rng flk = LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) and
A293: Plk = flk by Th43;
set beta = (((Pcm + Pml) + Plk) + Pkj) + Pjd;
A294: 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 A295: rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) is closed by RELAT_1:113;
A296: rng Pml misses V by A19, A29, A289, 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 object ; :: 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 A297: 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;
A298: (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 object 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, A82, XBOOLE_0:3;
hence contradiction by A10, A52, A286, A287, A288, CONNSP_1:35; :: thesis: verum
end;
A299: not LMP Jc in V by A17, A19, A289, XBOOLE_0:3;
not UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd) in V by A18, A41, A289, XBOOLE_0:3;
then {(LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))} misses V by A299, ZFMISC_1:51;
then A300: LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) misses V by A297, A298, XBOOLE_1:70;
A301: rng Pkj misses V by A50, A289, XBOOLE_1:63;
A302: LSeg ((LMP C),|[0,(- 3)]|) misses V by A1, A285, Th90;
LSeg (|[0,3]|,(UMP C)) misses V by A1, A285, Th89;
then ((LSeg (|[0,3]|,(UMP C))) \/ (rng Pml)) \/ (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) misses V by A296, A300, XBOOLE_1:114;
then A303: rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) misses V by A85, A86, A290, A291, A292, A293, A294, A301, A302, XBOOLE_1:114;
A304: UMP C = |[((UMP C) `1),((UMP C) `2)]| by EUCLID:53;
A305: |[0,3]| = |[(|[0,3]| `1),(|[0,3]| `2)]| by EUCLID:53;
A306: LMP C = |[((LMP C) `1),((LMP C) `2)]| by EUCLID:53;
A307: not |[(- 1),0]| in LSeg (|[0,3]|,(UMP C)) by A12, A13, A21, A23, A24, A304, A305, Lm16, JGRAPH_6:1;
not |[(- 1),0]| in rng Pml by A30, ZFMISC_1:49;
then A308: not |[(- 1),0]| in (LSeg (|[0,3]|,(UMP C))) \/ (rng Pml) by A307, XBOOLE_0:def 3;
not |[(- 1),0]| in LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) by A22, A44, A56, A57, A59, Lm16, JGRAPH_6:1;
then A309: not |[(- 1),0]| in ((LSeg (|[0,3]|,(UMP C))) \/ (rng Pml)) \/ (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) by A308, XBOOLE_0:def 3;
not |[(- 1),0]| in rng Pkj by A49, ZFMISC_1:49;
then A310: not |[(- 1),0]| in (((LSeg (|[0,3]|,(UMP C))) \/ (rng Pml)) \/ (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))))) \/ (rng Pkj) by A309, XBOOLE_0:def 3;
not |[(- 1),0]| in LSeg ((LMP C),|[0,(- 3)]|) by A34, A35, A58, A306, Lm16, Lm22, JGRAPH_6:1;
then not |[(- 1),0]| in rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A85, A86, A290, A291, A292, A293, A294, A310, XBOOLE_0:def 3;
then consider ra being positive Real such that
A311: Ball (|[(- 1),0]|,ra) misses rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A295, Th25;
A312: not |[1,0]| in LSeg (|[0,3]|,(UMP C)) by A12, A13, A21, A23, A24, A304, A305, Lm17, JGRAPH_6:1;
not |[1,0]| in rng Pml by A30, ZFMISC_1:49;
then A313: not |[1,0]| in (LSeg (|[0,3]|,(UMP C))) \/ (rng Pml) by A312, XBOOLE_0:def 3;
not |[1,0]| in LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))) by A22, A44, A56, A57, A59, Lm17, JGRAPH_6:1;
then A314: not |[1,0]| in ((LSeg (|[0,3]|,(UMP C))) \/ (rng Pml)) \/ (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)))) by A313, XBOOLE_0:def 3;
not |[1,0]| in rng Pkj by A49, ZFMISC_1:49;
then A315: not |[1,0]| in (((LSeg (|[0,3]|,(UMP C))) \/ (rng Pml)) \/ (LSeg ((LMP Jc),(UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd))))) \/ (rng Pkj) by A314, XBOOLE_0:def 3;
not |[1,0]| in LSeg ((LMP C),|[0,(- 3)]|) by A34, A35, A58, A306, Lm17, Lm22, JGRAPH_6:1;
then not |[1,0]| in rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A85, A86, A290, A291, A292, A293, A294, A315, XBOOLE_0:def 3;
then consider rb being positive Real such that
A316: Ball (|[1,0]|,rb) misses rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A295, Th25;
set A = Ball (|[(- 1),0]|,ra);
set B = Ball (|[1,0]|,rb);
A317: |[(- 1),0]| in Ball (|[(- 1),0]|,ra) by Th16;
A318: |[1,0]| in Ball (|[1,0]|,rb) by Th16;
not VP is empty ;
then consider t being object such that
A319: t in V by A287;
V in { W where W is Subset of (TOP-REAL 2) : W is_inside_component_of C } by A285;
then t in BDD C by A319, TARSKI:def 4;
then A320: C = Fr V by A287, A288, Lm15;
then |[(- 1),0]| in Cl V by A14, XBOOLE_0:def 4;
then Ball (|[(- 1),0]|,ra) meets V by A317, PRE_TOPC:def 7;
then consider u being object such that
A321: u in Ball (|[(- 1),0]|,ra) and
A322: u in V by XBOOLE_0:3;
|[1,0]| in Cl V by A15, A320, XBOOLE_0:def 4;
then Ball (|[1,0]|,rb) meets V by A318, PRE_TOPC:def 7;
then consider v being object such that
A323: v in Ball (|[1,0]|,rb) and
A324: v in V by XBOOLE_0:3;
reconsider u = u, v = v as Point of (TOP-REAL 2) by A321, A323;
A325: the carrier of (T2C | VP) = VP by PRE_TOPC:8;
reconsider u1 = u, v1 = v as Point of (T2C | VP) by A287, A322, A324, PRE_TOPC:8;
T2C | VP is pathwise_connected by A288, Th69;
then A326: u1,v1 are_connected ;
then consider fuv being Function of I[01],(T2C | VP) such that
A327: fuv is continuous and
A328: fuv . 0 = u1 and
A329: fuv . 1 = v1 ;
A330: T2C | VP = (TOP-REAL 2) | V by A287, GOBOARD9:2;
fuv is Path of u1,v1 by A326, A327, A328, A329, BORSUK_2:def 2;
then reconsider uv = fuv as Path of u,v by A326, A330, TOPALG_2:1;
A331: rng fuv c= the carrier of (T2C | VP) ;
then A332: rng uv misses rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A287, A303, A325, 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
A333: rng fau = LSeg (|[(- 1),0]|,u) and
A334: 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
A335: rng fvb = LSeg (v,|[1,0]|) and
A336: vb = fvb by Th43;
set AB = (au + uv) + vb;
A337: 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 A321, JORDAN1:def 1;
then A338: LSeg (|[(- 1),0]|,u) misses rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A311, XBOOLE_1:63;
|[1,0]| in Ball (|[1,0]|,rb) by Th16;
then LSeg (v,|[1,0]|) c= Ball (|[1,0]|,rb) by A323, JORDAN1:def 1;
then LSeg (v,|[1,0]|) misses rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A316, XBOOLE_1:63;
then A339: rng ((au + uv) + vb) misses rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A332, A333, A334, A335, A336, A337, A338, XBOOLE_1:114;
A340: |[(- 1),0]|,|[1,0]| are_connected by BORSUK_2:def 3;
A341: V c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A1, A285, Th93;
then A342: LSeg (|[(- 1),0]|,u) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A11, A14, A322, JORDAN1:def 1;
A343: LSeg (v,|[1,0]|) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A11, A15, A324, A341, JORDAN1:def 1;
rng uv c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A287, A325, A331, A341;
then (LSeg (|[(- 1),0]|,u)) \/ (rng uv) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A342, XBOOLE_1:8;
then rng ((au + uv) + vb) c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A84, A333, A334, A335, A336, A337, A343, XBOOLE_1:8;
then reconsider h = (au + uv) + vb as Path of AR,BR by A340, Th29;
A344: |[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 A87, A88, XBOOLE_1:8;
then A345: ((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 A83, XBOOLE_1:8;
rng Pkj c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A11, A50;
then A346: (((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 A345, 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 A84, A85, A86, A290, A291, A292, A293, A294, A346, XBOOLE_1:8;
then reconsider v = (((Pcm + Pml) + Plk) + Pkj) + Pjd as Path of CR,DR by A344, Th29;
consider s, t being Point of I[01] such that
A347: h . s = v . t by Lm16, Lm17, Lm21, Lm23, JGRAPH_8:6;
A348: dom h = the carrier of I[01] by FUNCT_2:def 1;
A349: dom v = the carrier of I[01] by FUNCT_2:def 1;
A350: h . s in rng ((au + uv) + vb) by A348, FUNCT_1:def 3;
v . t in rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A349, FUNCT_1:def 3;
hence contradiction by A339, A347, A350, XBOOLE_0:3; :: thesis: verum