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 & |[1,0 ]| in C ) by A1, JORDAN24:def 1;
A15: UMP C in C by JORDAN21:43;
A16: LMP Jc in Jc by JORDAN21:44;
A17: Jd c= C by A4, XBOOLE_1:7;
A18: Jc c= C by A4, XBOOLE_1:7;
then A19: LMP Jc in C by A16;
A20: (UMP C) `2 < |[0 ,3]| `2 by A1, Lm23, Th83, JORDAN21:43;
A21: (LMP Jc) `1 = 0 by A8, A9, A12, A13, EUCLID:56;
A22: |[0 ,3]| `1 = ((W-bound C) + (E-bound C)) / 2 by A1, Lm81;
A23: (UMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;
A24: ( UMP C <> |[(- 1),0 ]| & UMP C <> |[1,0 ]| & LMP Jc <> |[(- 1),0 ]| & LMP Jc <> |[1,0 ]| ) by A8, A9, A12, A13, Lm18, Lm19, EUCLID:56;
then consider Pml being Path of UMP C, LMP Jc such that
A25: rng Pml c= Jc and
A26: rng Pml misses {|[(- 1),0 ]|,|[1,0 ]|} by A2, A6, A16, Th44;
set ml = rng Pml;
A27: rng Pml c= C by A18, A25, XBOOLE_1:1;
A28: LMP C in C by A7, A17;
A29: LSeg (LMP Jc),|[0 ,(- 3)]| is vertical by A21, Lm24, SPPOL_1:37;
A30: |[0 ,(- 3)]| `2 <= (LMP C) `2 by A1, A7, A17, Lm25, Th84;
A31: (LMP C) `1 = 0 by A12, A13, EUCLID:56;
LMP Jc in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A12, A13, A21, JORDAN6:34;
then A32: LMP Jc in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) by A16, A18, XBOOLE_0:def 4;
then (LMP C) `2 <= (LMP Jc) `2 by JORDAN21:42;
then LMP C in LSeg (LMP Jc),|[0 ,(- 3)]| by A21, A30, A31, Lm24, GOBOARD7:8;
then A33: not (LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd is empty by A7, XBOOLE_0:def 4;
A34: (LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd is compact by COMPTS_1:20;
A36: (LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd is vertical by A29, Th4;
then (LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd is with_the_max_arc by A33, A34;
then A37: UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) in (LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd by A34, JORDAN21:43;
then A38: UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) in LSeg (LMP Jc),|[0 ,(- 3)]| by XBOOLE_0:def 4;
A39: UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) in Jd by A37, XBOOLE_0:def 4;
then A40: UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) in C by A17;
A41: |[0 ,(- 3)]| in LSeg (LMP Jc),|[0 ,(- 3)]| by RLTOPSP1:69;
then A42: (UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) `1 = 0 by A29, A38, Lm24, SPPOL_1:def 3;
then ( UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) <> |[(- 1),0 ]| & UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) <> |[1,0 ]| & LMP C <> |[(- 1),0 ]| & LMP C <> |[1,0 ]| ) by A31, EUCLID:56;
then consider Pkj being Path of UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd), LMP C such that
A43: rng Pkj c= Jd and
A44: rng Pkj misses {|[(- 1),0 ]|,|[1,0 ]|} by A3, A7, A39, Th44;
set kj = rng Pkj;
A45: rng Pkj c= C by A17, A43, XBOOLE_1:1;
A46: (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;
A47: Component_of (Down ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))),(C ` )) is_a_component_of (TOP-REAL 2) | (C ` ) by CONNSP_1:43;
A48: the carrier of ((TOP-REAL 2) | (C ` )) = C ` by PRE_TOPC:29;
A49: LSeg (LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) is vertical by A21, A42, SPPOL_1:37;
A50: UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) in LSeg (LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) by RLTOPSP1:69;
A51: ( LMP Jc = |[((LMP Jc) `1 ),((LMP Jc) `2 )]| & 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;
A52: |[0 ,(- 3)]| = |[(|[0 ,(- 3)]| `1 ),(|[0 ,(- 3)]| `2 )]| by EUCLID:57;
|[0 ,(- 3)]| `2 <= (LMP Jc) `2 by A1, A16, A18, Lm25, Th84;
then A53: (UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) `2 <= (LMP Jc) `2 by A21, A38, A51, A52, Lm24, JGRAPH_6:9;
( |[(- 1),0 ]| <> UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) & |[1,0 ]| <> UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) & |[(- 1),0 ]| <> LMP Jc & |[1,0 ]| <> LMP Jc ) by A21, A42, EUCLID:56;
then ( not UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) in {|[(- 1),0 ]|,|[1,0 ]|} & not LMP Jc in {|[(- 1),0 ]|,|[1,0 ]|} ) by TARSKI:def 2;
then A54: UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) <> LMP Jc by A5, A16, A39, XBOOLE_0:def 4;
then (UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) `2 <> (LMP Jc) `2 by A21, A42, TOPREAL3:11;
then A55: (UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) `2 < (LMP Jc) `2 by A53, XXREAL_0:1;
UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A12, A13, A42, JORDAN6:34;
then UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) by A17, A39, 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, A17, Lm25, Th84, XXREAL_0:2;
then A56: LSeg (LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) c= LSeg (LMP Jc),|[0 ,(- 3)]| by A29, A42, A49, A53, Lm24, GOBOARD7:65;
A57: (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
A58: q in (LSeg (LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd))) \ {(LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd))} and
A59: not q in C ` ; :: thesis: contradiction
A60: q in LSeg (LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) by A58, XBOOLE_0:def 5;
reconsider q = q as Point of (TOP-REAL 2) by A58;
A61: q in C by A59, SUBSET_1:50;
A62: q `1 = ((W-bound C) + (E-bound C)) / 2 by A12, A13, A42, A49, A50, A60, SPPOL_1:def 3;
then A63: 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, A61, XBOOLE_0:def 3;
suppose q in Jd ; :: thesis: contradiction
then A65: q in (LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd by A56, A60, XBOOLE_0:def 4;
A66: q `1 = |[0 ,(- 3)]| `1 by A29, A41, A56, A60, SPPOL_1:def 3;
(LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd c= LSeg (LMP Jc),|[0 ,(- 3)]| by XBOOLE_1:17;
then A67: ( W-bound (LSeg (LMP Jc),|[0 ,(- 3)]|) <= W-bound ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) & E-bound ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) <= E-bound (LSeg (LMP Jc),|[0 ,(- 3)]|) ) by A65, PSCOMP_1:130, PSCOMP_1:132;
A68: W-bound ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) = E-bound ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) by A33, A34, A36, SPRECT_1:17;
A69: ( W-bound (LSeg (LMP Jc),|[0 ,(- 3)]|) = |[0 ,(- 3)]| `1 & E-bound (LSeg (LMP Jc),|[0 ,(- 3)]|) = |[0 ,(- 3)]| `1 ) by A21, Lm24, SPRECT_1:62, SPRECT_1:65;
then ( W-bound (LSeg (LMP Jc),|[0 ,(- 3)]|) = W-bound ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) & E-bound (LSeg (LMP Jc),|[0 ,(- 3)]|) = E-bound ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) ) by A67, A68, XXREAL_0:1;
then q in Vertical_Line (((W-bound ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (E-bound ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd))) / 2) by A66, A69, 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 A65, XBOOLE_0:def 4;
then A70: q `2 <= (UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) `2 by A34, JORDAN21:41;
(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) `2 <= q `2 by A21, A42, A51, A53, A60, JGRAPH_6:9;
then (UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) `2 = q `2 by A70, XXREAL_0:1;
then UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) = q by A12, A13, A42, A62, TOPREAL3:11;
then q in {(LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd))} by TARSKI:def 2;
hence contradiction by A58, 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 A54, Th1; :: thesis: verum
end;
then A71: (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 A46, 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 A57, CONNSP_3:27;
then A72: (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 A57, A71, CONNSP_3:26;
then A73: X meets Ux by A10, A71, 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 A74: X c= Component_of (Down ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))),(C ` )) by A10, A47, A73, CONNSP_1:38;
A75: LSeg (LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) c= closed_inside_of_rectangle (- 1),1,(- 3),3 by A11, A19, A40, JORDAN1:def 1;
A76: 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, Lm60, Lm61, Lm65, 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
A77: ( rng fcm = LSeg |[0 ,3]|,(UMP C) & Pcm = fcm ) by Th43;
A78: LSeg |[0 ,3]|,(UMP C) c= closed_inside_of_rectangle (- 1),1,(- 3),3 by A11, A15, Lm60, Lm65, JORDAN1:def 1;
A79: rng Pml c= closed_inside_of_rectangle (- 1),1,(- 3),3 by A11, A27, 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 A80: Ux is_a_component_of C ` by A10, A47, 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
A81: u in Ux and
A82: not u in Ball ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))),10 by TARSKI:def 3;
A83: closed_inside_of_rectangle (- 1),1,(- 3),3 c= Ball ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))),10 by A46, A75, Lm83;
reconsider u = u as Point of (TOP-REAL 2) by A81;
A84: Ux is open by A80, SPRECT_3:18;
Component_of (Down ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))),(C ` )) is connected by A47, CONNSP_1:def 5;
then Ux is connected by A10, CONNSP_1:24;
then A85: Ux is being_Region by A84;
(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
A86: P1 is_S-P_arc_joining (1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc)),u and
A87: P1 c= Ux by A10, A72, A81, A82, A85, TOPREAL4:30;
A88: P1 is_an_arc_of (1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc)),u by A86, TOPREAL4:3;
reconsider P2 = P1 as Subset of ((TOP-REAL 2) | (C ` )) by A10, A87, XBOOLE_1:1;
A89: P2 c= Component_of (Down ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))),(C ` )) by A10, A87;
A90: P2 misses C by A48, SUBSET_1:43;
then A91: P2 misses Jc by A4, XBOOLE_1:7, XBOOLE_1:63;
A92: P2 misses Jd by A4, A90, XBOOLE_1:7, XBOOLE_1:63;
A93: ((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 A21, A42 ;
then A94: LSeg |[0 ,(- 3)]|,((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))) is vertical by Lm24, SPPOL_1:37;
A95: (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;
A96: ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))) `2 < (LMP Jc) `2 by A55, Th3;
A97: (UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) `2 < ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))) `2 by A55, Th2;
then A98: |[0 ,(- 3)]| `2 <= ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))) `2 by A1, A17, A39, Lm25, Th84, XXREAL_0:2;
|[0 ,(- 3)]| `1 = |[0 ,(- 3)]| `1 ;
then A99: LSeg |[0 ,(- 3)]|,((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))) c= LSeg |[0 ,(- 3)]|,(LMP Jc) by A29, A94, A96, A98, GOBOARD7:65;
A100: 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
A101: q in LSeg |[0 ,(- 3)]|,((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))) and
A102: q in Jc by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A101;
q `2 <= ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))) `2 by A52, A93, A95, A98, A101, Lm24, JGRAPH_6:9;
then A103: q `2 < (LMP Jc) `2 by A96, XXREAL_0:2;
q `1 = 0 by A29, A41, A99, A101, Lm24, 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 A102, XBOOLE_0:def 4;
hence contradiction by A8, A9, A103, 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);
A104: not u in closed_inside_of_rectangle (- 1),1,(- 3),3 by A82, A83;
A105: Fr (closed_inside_of_rectangle (- 1),1,(- 3),3) = rectangle (- 1),1,(- 3),3 by Th52;
u in P1 by A88, TOPREAL1:4;
then A106: P1 \ (closed_inside_of_rectangle (- 1),1,(- 3),3) <> {} (TOP-REAL 2) by A104, XBOOLE_0:def 5;
(1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc)) in P1 by A88, TOPREAL1:4;
then P1 meets closed_inside_of_rectangle (- 1),1,(- 3),3 by A46, A75, XBOOLE_0:3;
then A107: P1 meets rectangle (- 1),1,(- 3),3 by A88, A105, A106, CONNSP_1:23, JORDAN6:11;
P1 is closed by A86, JORDAN6:12, TOPREAL4:3;
then P1 /\ (rectangle (- 1),1,(- 3),3) is closed by TOPS_1:35;
then A108: 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 A88, A107, JORDAN5C:def 1;
then A109: 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;
A110: First_Point P1,((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))),u,(rectangle (- 1),1,(- 3),3) in P1 by A108, 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));
A111: - 3 < (UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) `2 by A1, A17, A39, Th84;
(LMP Jc) `2 <= (UMP C) `2 by A32, JORDAN21:41;
then ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))) `2 < (UMP C) `2 by A96, XXREAL_0:2;
then not (1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc)) in rectangle (- 1),1,(- 3),3 by A20, A93, A95, A97, A111, Lm80;
then A112: 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 A86, A109, A110, JORDAN16:39, TOPREAL4:3;
A113: 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 A91, JORDAN16:5, XBOOLE_1:63;
A114: 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 A92, 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
A115: ( rng fdx = LSeg |[0 ,(- 3)]|,((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))) & 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
A116: ( rng fJc = Jc & 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
A117: ( rng fJd = Jd & 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
A118: ( 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)) & Palpha = falpha ) by A112, 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 A109, Lm65;
then A119: 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, A18, A76, A116, 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, A17, A76, A117, XBOOLE_1:1;
then reconsider H = PJd as Path of AR,BR by Th30;
A120: LSeg |[0 ,(- 3)]|,((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))) c= closed_inside_of_rectangle (- 1),1,(- 3),3 by A46, A75, Lm61, Lm65, JORDAN1:def 1;
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)) c= closed_inside_of_rectangle (- 1),1,(- 3),3 by A46, A75, A86, A104, Th57, TOPREAL4:3;
A122: |[(- 1),(- 3)]| in LSeg |[(- 1),(- 3)]|,|[(- 1),3]| by RLTOPSP1:69;
A123: |[1,(- 3)]| in LSeg |[1,(- 3)]|,|[1,3]| by RLTOPSP1:69;
LSeg |[(- 1),3]|,|[0 ,3]| misses C by A1, Lm72;
then A124: LSeg |[(- 1),3]|,|[0 ,3]| misses Jc by A4, XBOOLE_1:7, XBOOLE_1:63;
A125: LSeg |[(- 1),3]|,|[0 ,3]| c= closed_inside_of_rectangle (- 1),1,(- 3),3 by Lm65, Lm66, XBOOLE_1:1;
A126: LSeg |[1,3]|,|[0 ,3]| c= closed_inside_of_rectangle (- 1),1,(- 3),3 by Lm65, Lm67, XBOOLE_1:1;
LSeg |[1,3]|,|[0 ,3]| misses C by A1, Lm73;
then A127: 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
A128: ( rng flx = LSeg (LMP Jc),((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))) & Plx = flx ) by Th43;
set PCX = (Pcm + Pml) + Plx;
A129: rng ((Pcm + Pml) + Plx) = ((rng Pcm) \/ (rng Pml)) \/ (rng Plx) by Th40;
A130: rng Pml misses Jd
proof
assume rng Pml meets Jd ; :: thesis: contradiction
then consider q being set such that
A131: q in rng Pml and
A132: q in Jd by XBOOLE_0:3;
q in {|[(- 1),0 ]|,|[1,0 ]|} by A5, A25, A131, A132, XBOOLE_0:def 4;
hence contradiction by A26, A131, XBOOLE_0:3; :: thesis: verum
end;
A133: (LSeg |[0 ,3]|,(UMP C)) /\ C = {(UMP C)} by A1, Th91;
A134: 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
A135: q in LSeg |[0 ,3]|,(UMP C) and
A136: q in Jd by XBOOLE_0:3;
q in {(UMP C)} by A17, A133, A135, A136, XBOOLE_0:def 4;
then q = UMP C by TARSKI:def 1;
then UMP C in {|[(- 1),0 ]|,|[1,0 ]|} by A5, A6, A136, XBOOLE_0:def 4;
hence contradiction by A24, TARSKI:def 2; :: thesis: verum
end;
LSeg (LMP Jc),((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))) is vertical by A21, A93, SPPOL_1:37;
then A137: 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 A42, A49, A93, A96, A97, 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 A138: 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 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 A139: ( q in LSeg (LMP Jc),((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))) & q <> LMP Jc ) by ZFMISC_1:64;
then q <> UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) by A21, A51, A93, A95, A96, A97, JGRAPH_6:9;
then not q in {(LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd))} by A139, 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 A137, A139, 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 A57, 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 A140: (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, A16, XBOOLE_0:def 4;
hence contradiction by A24, TARSKI:def 2; :: thesis: verum
end;
then LSeg (LMP Jc),((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))) misses Jd by A138, A140, XBOOLE_1:70;
then A141: rng ((Pcm + Pml) + Plx) misses Jd by A77, A128, A129, A130, A134, 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 A75, A137, XBOOLE_1:1;
then A142: rng ((Pcm + Pml) + Plx) c= closed_inside_of_rectangle (- 1),1,(- 3),3 by A77, A78, A79, A128, A129, Lm1;
LSeg |[(- 1),(- 3)]|,|[0 ,(- 3)]| misses C by A1, Lm74;
then A143: LSeg |[(- 1),(- 3)]|,|[0 ,(- 3)]| misses Jd by A4, XBOOLE_1:7, XBOOLE_1:63;
LSeg |[1,(- 3)]|,|[0 ,(- 3)]| misses C by A1, Lm75;
then A144: 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 A145: (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 A109, A145, Lm71;
suppose A146: 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
A147: ( 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)]| & 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
A148: ( rng fldd = LSeg |[(- 1),(- 3)]|,|[0 ,(- 3)]| & Pldd = fldd ) by Th43;
A149: |[(- 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 A122, A146, Lm43, Lm56, 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 A119, A149, Lm27, Lm29, Lm43, GOBOARD7:65;
then A150: 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 Lm39, 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, A48, A89, A110, A146, Lm78;
then A151: 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;
A152: rng (((((Pcm + Pml) + Plx) + Palpha) + Pnld) + Pldd) = (((rng ((Pcm + Pml) + Plx)) \/ (rng Palpha)) \/ (rng Pnld)) \/ (rng Pldd) by Lm11;
then A153: rng PJd misses rng (((((Pcm + Pml) + Plx) + Palpha) + Pnld) + Pldd) by A114, A117, A118, A141, A143, A147, A148, A151, Lm3;
A154: LSeg |[(- 1),(- 3)]|,|[0 ,(- 3)]| c= closed_inside_of_rectangle (- 1),1,(- 3),3 by Lm65, Lm68, 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 A150, Lm65, XBOOLE_1:1;
then rng (((((Pcm + Pml) + Plx) + Palpha) + Pnld) + Pldd) c= the carrier of (Trectangle (- 1),1,(- 3),3) by A76, A118, A121, A142, A147, A148, A152, A154, 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
A155: H . s = v . t by Lm18, Lm19, Lm23, Lm25, JGRAPH_8:6;
( dom H = the carrier of I[01] & dom v = the carrier of I[01] ) by FUNCT_2:def 1;
then ( H . s in rng PJd & v . t in rng (((((Pcm + Pml) + Plx) + Palpha) + Pnld) + Pldd) ) by FUNCT_1:def 5;
hence contradiction by A153, A155, XBOOLE_0:3; :: thesis: verum
end;
suppose A156: 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
A157: ( 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)]| & Pnd = fnd ) by Th43;
set K1 = (((Pcm + Pml) + Plx) + Palpha) + Pnd;
|[(- 1),(- 3)]| in LSeg |[(- 1),(- 3)]|,|[0 ,(- 3)]| by RLTOPSP1:69;
then A158: |[(- 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 A156, Lm49, SPPOL_1:def 2;
then A159: 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 Lm25, Lm29, SPPOL_1:36;
( |[(- 1),(- 3)]| `1 <= (First_Point P1,((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))),u,(rectangle (- 1),1,(- 3),3)) `1 & (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 A156, Lm24, Lm28, JGRAPH_6:11;
then A160: 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 A158, A159, Lm49, GOBOARD7:66;
then A161: 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 Lm68, 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, A160, Lm74, XBOOLE_1:63;
then A162: 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;
A163: rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) = ((rng ((Pcm + Pml) + Plx)) \/ (rng Palpha)) \/ (rng Pnd) by Th40;
then A164: rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) misses Jd by A114, A118, A141, A157, A162, 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 A161, Lm65, XBOOLE_1:1;
then rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) c= the carrier of (Trectangle (- 1),1,(- 3),3) by A76, A118, A121, A142, A157, A163, 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
A165: H . s = v . t by Lm18, Lm19, Lm23, Lm25, JGRAPH_8:6;
( dom H = the carrier of I[01] & dom v = the carrier of I[01] ) by FUNCT_2:def 1;
then ( H . s in rng PJd & v . t in rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) ) by FUNCT_1:def 5;
hence contradiction by A117, A164, A165, XBOOLE_0:3; :: thesis: verum
end;
suppose A166: 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
A167: ( 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)]| & 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 A166, Lm50, SPPOL_1:def 2;
then A168: 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 Lm25, Lm33, SPPOL_1:36;
A169: |[0 ,(- 3)]| `2 = |[0 ,(- 3)]| `2 ;
( |[0 ,(- 3)]| `1 <= (First_Point P1,((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))),u,(rectangle (- 1),1,(- 3),3)) `1 & (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 A166, Lm24, Lm32, JGRAPH_6:11;
then A170: 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 A168, A169, Lm50, GOBOARD7:66;
then A171: 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 Lm69, 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, A170, Lm75, XBOOLE_1:63;
then A172: 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;
A173: rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) = ((rng ((Pcm + Pml) + Plx)) \/ (rng Palpha)) \/ (rng Pnd) by Th40;
then A174: rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) misses Jd by A114, A118, A141, A167, A172, 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 A171, Lm65, XBOOLE_1:1;
then rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) c= the carrier of (Trectangle (- 1),1,(- 3),3) by A76, A118, A121, A142, A167, A173, 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
A175: H . s = v . t by Lm18, Lm19, Lm23, Lm25, JGRAPH_8:6;
( dom H = the carrier of I[01] & dom v = the carrier of I[01] ) by FUNCT_2:def 1;
then ( H . s in rng PJd & v . t in rng ((((Pcm + Pml) + Plx) + Palpha) + Pnd) ) by FUNCT_1:def 5;
hence contradiction by A117, A174, A175, XBOOLE_0:3; :: thesis: verum
end;
suppose A176: 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
A177: ( 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)]| & 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
A178: ( rng fpdd = LSeg |[1,(- 3)]|,|[0 ,(- 3)]| & Ppdd = fpdd ) by Th43;
A179: |[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 A123, A176, Lm44, 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 A119, A179, Lm31, Lm33, Lm44, GOBOARD7:65;
then A180: 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 Lm41, 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, A48, A89, A110, A176, Lm79;
then A181: 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;
A182: rng (((((Pcm + Pml) + Plx) + Palpha) + Pnpd) + Ppdd) = (((rng ((Pcm + Pml) + Plx)) \/ (rng Palpha)) \/ (rng Pnpd)) \/ (rng Ppdd) by Lm11;
then A183: rng PJd misses rng (((((Pcm + Pml) + Plx) + Palpha) + Pnpd) + Ppdd) by A114, A117, A118, A141, A144, A177, A178, A181, Lm3;
A184: LSeg |[1,(- 3)]|,|[0 ,(- 3)]| c= closed_inside_of_rectangle (- 1),1,(- 3),3 by Lm65, Lm69, 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 A180, Lm65, XBOOLE_1:1;
then rng (((((Pcm + Pml) + Plx) + Palpha) + Pnpd) + Ppdd) c= the carrier of (Trectangle (- 1),1,(- 3),3) by A76, A118, A121, A142, A177, A178, A182, A184, 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
A185: H . s = v . t by Lm18, Lm19, Lm23, Lm25, JGRAPH_8:6;
( dom H = the carrier of I[01] & dom v = the carrier of I[01] ) by FUNCT_2:def 1;
then ( H . s in rng PJd & v . t in rng (((((Pcm + Pml) + Plx) + Palpha) + Pnpd) + Ppdd) ) by FUNCT_1:def 5;
hence contradiction by A183, A185, XBOOLE_0:3; :: thesis: verum
end;
end;
end;
suppose A186: (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 A109, A186, Lm70;
suppose A187: 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
A188: ( 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]| & 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
A189: ( rng flgc = LSeg |[(- 1),3]|,|[0 ,3]| & Plgc = flgc ) by Th43;
A190: |[(- 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 A122, A187, Lm43, Lm55, 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 Lm26, Lm28, 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 A119, A190, Lm27, Lm29, Lm43, GOBOARD7:65;
then A191: 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 Lm39, 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, A48, A89, A110, A187, Lm76;
then A192: 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;
A193: rng (((Pdx + Palpha) + Pnlg) + Plgc) = (((rng Pdx) \/ (rng Palpha)) \/ (rng Pnlg)) \/ (rng Plgc) by Lm11;
then A194: rng (((Pdx + Palpha) + Pnlg) + Plgc) misses Jc by A100, A113, A115, A118, A124, A188, A189, A192, Lm3;
A195: 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 A191, Lm65, XBOOLE_1:1;
then rng (((Pdx + Palpha) + Pnlg) + Plgc) c= the carrier of (Trectangle (- 1),1,(- 3),3) by A76, A115, A118, A120, A121, A125, A188, A189, A193, Lm2;
then reconsider v = - (((Pdx + Palpha) + Pnlg) + Plgc) as Path of CR,DR by A195, Th30;
consider s, t being Point of I[01] such that
A196: h . s = v . t by Lm18, Lm19, Lm23, Lm25, JGRAPH_8:6;
( dom h = the carrier of I[01] & dom v = the carrier of I[01] ) by FUNCT_2:def 1;
then ( h . s in rng PJc & v . t in rng (- (((Pdx + Palpha) + Pnlg) + Plgc)) ) by FUNCT_1:def 5;
hence contradiction by A116, A194, A195, A196, XBOOLE_0:3; :: thesis: verum
end;
suppose A197: 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
A198: ( 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]| & Pnc = fnc ) by Th43;
set K1 = (Pdx + Palpha) + Pnc;
|[(- 1),3]| in LSeg |[(- 1),3]|,|[0 ,3]| by RLTOPSP1:69;
then A199: |[(- 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 A197, Lm51, SPPOL_1:def 2;
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]| is horizontal by Lm23, Lm27, SPPOL_1:36;
( |[(- 1),3]| `1 <= (First_Point P1,((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))),u,(rectangle (- 1),1,(- 3),3)) `1 & (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 A197, Lm22, Lm26, JGRAPH_6:11;
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]| c= LSeg |[(- 1),3]|,|[0 ,3]| by A199, A200, Lm51, GOBOARD7:66;
then A202: 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 Lm66, 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, A201, Lm72, XBOOLE_1:63;
then A203: 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;
A204: rng ((Pdx + Palpha) + Pnc) = ((rng Pdx) \/ (rng Palpha)) \/ (rng Pnc) by Th40;
then A205: rng ((Pdx + Palpha) + Pnc) misses Jc by A100, A113, A115, A118, A198, A203, XBOOLE_1:114;
A206: 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 A202, Lm65, XBOOLE_1:1;
then rng ((Pdx + Palpha) + Pnc) c= the carrier of (Trectangle (- 1),1,(- 3),3) by A76, A115, A118, A120, A121, A198, A204, Lm1;
then reconsider v = - ((Pdx + Palpha) + Pnc) as Path of CR,DR by A206, Th30;
consider s, t being Point of I[01] such that
A207: h . s = v . t by Lm18, Lm19, Lm23, Lm25, JGRAPH_8:6;
( dom h = the carrier of I[01] & dom v = the carrier of I[01] ) by FUNCT_2:def 1;
then ( h . s in rng PJc & v . t in rng (- ((Pdx + Palpha) + Pnc)) ) by FUNCT_1:def 5;
hence contradiction by A116, A205, A206, 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 |[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
A209: ( 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]| & 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 A208, Lm52, SPPOL_1:def 2;
then A210: 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;
A211: |[0 ,3]| `2 = |[0 ,3]| `2 ;
( |[0 ,3]| `1 <= (First_Point P1,((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))),u,(rectangle (- 1),1,(- 3),3)) `1 & (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 A208, Lm22, Lm30, JGRAPH_6:11;
then A212: 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 A210, A211, Lm52, GOBOARD7:66;
then A213: 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 Lm67, 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, A212, Lm73, XBOOLE_1:63;
then A214: 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;
A215: rng ((Pdx + Palpha) + Pnc) = ((rng Pdx) \/ (rng Palpha)) \/ (rng Pnc) by Th40;
then A216: rng ((Pdx + Palpha) + Pnc) misses Jc by A100, A113, A115, A118, A209, A214, XBOOLE_1:114;
A217: 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 A213, Lm65, XBOOLE_1:1;
then rng ((Pdx + Palpha) + Pnc) c= the carrier of (Trectangle (- 1),1,(- 3),3) by A76, A115, A118, A120, A121, A209, A215, Lm1;
then reconsider v = - ((Pdx + Palpha) + Pnc) as Path of CR,DR by A217, Th30;
consider s, t being Point of I[01] such that
A218: h . s = v . t by Lm18, Lm19, Lm23, Lm25, JGRAPH_8:6;
( dom h = the carrier of I[01] & dom v = the carrier of I[01] ) by FUNCT_2:def 1;
then ( h . s in rng PJc & v . t in rng (- ((Pdx + Palpha) + Pnc)) ) by FUNCT_1:def 5;
hence contradiction by A116, A216, A217, A218, XBOOLE_0:3; :: thesis: verum
end;
suppose A219: 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
A220: ( 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]| & 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
A221: ( rng fpgc = LSeg |[1,3]|,|[0 ,3]| & Ppgc = fpgc ) by Th43;
A222: |[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 A123, A219, Lm44, 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 Lm30, Lm32, 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 A119, A222, Lm31, Lm33, Lm44, GOBOARD7:65;
then A223: 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 Lm41, 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, A48, A89, A110, A219, Lm77;
then A224: 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;
A225: rng (((Pdx + Palpha) + Pnpg) + Ppgc) = (((rng Pdx) \/ (rng Palpha)) \/ (rng Pnpg)) \/ (rng Ppgc) by Lm11;
then A226: rng (((Pdx + Palpha) + Pnpg) + Ppgc) misses Jc by A100, A113, A115, A118, A127, A220, A221, A224, Lm3;
A227: 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 A223, Lm65, XBOOLE_1:1;
then rng (((Pdx + Palpha) + Pnpg) + Ppgc) c= the carrier of (Trectangle (- 1),1,(- 3),3) by A76, A115, A118, A120, A121, A126, A220, A221, A225, Lm2;
then reconsider v = - (((Pdx + Palpha) + Pnpg) + Ppgc) as Path of CR,DR by A227, Th30;
consider s, t being Point of I[01] such that
A228: h . s = v . t by Lm18, Lm19, Lm23, Lm25, JGRAPH_8:6;
( dom h = the carrier of I[01] & dom v = the carrier of I[01] ) by FUNCT_2:def 1;
then ( h . s in rng PJc & v . t in rng (- (((Pdx + Palpha) + Pnpg) + Ppgc)) ) by FUNCT_1:def 5;
hence contradiction by A116, A226, A227, A228, 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 A229: V is_inside_component_of C ; :: thesis: V = Ux
assume A230: V <> Ux ; :: thesis: contradiction
consider VP being Subset of ((TOP-REAL 2) | (C ` )) such that
A231: VP = V and
A232: VP is_a_component_of (TOP-REAL 2) | (C ` ) and
VP is bounded Subset of (Euclid 2) by A229, JORDAN2C:17;
reconsider T2C = (TOP-REAL 2) | (C ` ) as non empty SubSpace of TOP-REAL 2 ;
VP <> {} ((TOP-REAL 2) | (C ` )) by A232, CONNSP_1:34;
then reconsider VP = VP as non empty Subset of T2C ;
A233: V misses C by A48, A231, 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
A234: ( rng fjd = LSeg (LMP C),|[0 ,(- 3)]| & 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
A235: ( rng flk = LSeg (LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) & Plk = flk ) by Th43;
set beta = (((Pcm + Pml) + Plk) + Pkj) + Pjd;
A236: rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) = ((((rng Pcm) \/ (rng Pml)) \/ (rng Plk)) \/ (rng Pkj)) \/ (rng Pjd) by Lm13;
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 rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) is compact by RELAT_1:146;
then A237: rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) is closed ;
A238: rng Pml misses V by A27, A233, 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 A239: 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;
A240: (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 consider q being set such that
A241: q in (LSeg (LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd))) \ {(LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd))} and
A242: q in V by XBOOLE_0:3;
V meets Ux by A10, A74, A241, A242, XBOOLE_0:3;
hence contradiction by A10, A47, A230, A231, A232, CONNSP_1:37; :: thesis: verum
end;
( not LMP Jc in V & not UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd) in V ) by A16, A17, A18, A39, A233, XBOOLE_0:3;
then {(LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd))} misses V by ZFMISC_1:57;
then A243: LSeg (LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) misses V by A239, A240, XBOOLE_1:70;
A244: rng Pkj misses V by A45, A233, XBOOLE_1:63;
A245: LSeg (LMP C),|[0 ,(- 3)]| misses V by A1, A229, Th90;
LSeg |[0 ,3]|,(UMP C) misses V by A1, A229, Th89;
then ((LSeg |[0 ,3]|,(UMP C)) \/ (rng Pml)) \/ (LSeg (LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd))) misses V by A238, A243, XBOOLE_1:114;
then A246: rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) misses V by A77, A234, A235, A236, A244, A245, XBOOLE_1:114;
A247: UMP C = |[((UMP C) `1 ),((UMP C) `2 )]| by EUCLID:57;
A248: |[0 ,3]| = |[(|[0 ,3]| `1 ),(|[0 ,3]| `2 )]| by EUCLID:57;
A249: LMP C = |[((LMP C) `1 ),((LMP C) `2 )]| by EUCLID:57;
A250: not |[(- 1),0 ]| in LSeg |[0 ,3]|,(UMP C) by A12, A13, A20, A22, A23, A247, A248, Lm18, JGRAPH_6:9;
not |[(- 1),0 ]| in rng Pml by A26, ZFMISC_1:55;
then A251: not |[(- 1),0 ]| in (LSeg |[0 ,3]|,(UMP C)) \/ (rng Pml) by A250, XBOOLE_0:def 3;
not |[(- 1),0 ]| in LSeg (LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) by A21, A42, A51, A53, Lm18, JGRAPH_6:9;
then A252: not |[(- 1),0 ]| in ((LSeg |[0 ,3]|,(UMP C)) \/ (rng Pml)) \/ (LSeg (LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd))) by A251, XBOOLE_0:def 3;
not |[(- 1),0 ]| in rng Pkj by A44, ZFMISC_1:55;
then A253: not |[(- 1),0 ]| in (((LSeg |[0 ,3]|,(UMP C)) \/ (rng Pml)) \/ (LSeg (LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)))) \/ (rng Pkj) by A252, XBOOLE_0:def 3;
not |[(- 1),0 ]| in LSeg (LMP C),|[0 ,(- 3)]| by A30, A31, A52, A249, Lm18, Lm24, JGRAPH_6:9;
then not |[(- 1),0 ]| in rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A77, A234, A235, A236, A253, XBOOLE_0:def 3;
then consider ra being positive real number such that
A254: Ball |[(- 1),0 ]|,ra misses rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A237, Th25;
A255: not |[1,0 ]| in LSeg |[0 ,3]|,(UMP C) by A12, A13, A20, A22, A23, A247, A248, Lm19, JGRAPH_6:9;
not |[1,0 ]| in rng Pml by A26, ZFMISC_1:55;
then A256: not |[1,0 ]| in (LSeg |[0 ,3]|,(UMP C)) \/ (rng Pml) by A255, XBOOLE_0:def 3;
not |[1,0 ]| in LSeg (LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) by A21, A42, A51, A53, Lm19, JGRAPH_6:9;
then A257: not |[1,0 ]| in ((LSeg |[0 ,3]|,(UMP C)) \/ (rng Pml)) \/ (LSeg (LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd))) by A256, XBOOLE_0:def 3;
not |[1,0 ]| in rng Pkj by A44, ZFMISC_1:55;
then A258: not |[1,0 ]| in (((LSeg |[0 ,3]|,(UMP C)) \/ (rng Pml)) \/ (LSeg (LMP Jc),(UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)))) \/ (rng Pkj) by A257, XBOOLE_0:def 3;
not |[1,0 ]| in LSeg (LMP C),|[0 ,(- 3)]| by A30, A31, A52, A249, Lm19, Lm24, JGRAPH_6:9;
then not |[1,0 ]| in rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A77, A234, A235, A236, A258, XBOOLE_0:def 3;
then consider rb being positive real number such that
A259: Ball |[1,0 ]|,rb misses rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A237, Th25;
set A = Ball |[(- 1),0 ]|,ra;
set B = Ball |[1,0 ]|,rb;
A260: |[(- 1),0 ]| in Ball |[(- 1),0 ]|,ra by Th16;
A261: |[1,0 ]| in Ball |[1,0 ]|,rb by Th16;
not VP is empty ;
then consider t being set such that
A262: t in V by A231, XBOOLE_0:def 1;
V in { W where W is Subset of (TOP-REAL 2) : W is_inside_component_of C } by A229;
then t in BDD C by A262, TARSKI:def 4;
then A263: C = Fr V by A231, A232, Lm17;
then |[(- 1),0 ]| in Cl V by A14, XBOOLE_0:def 4;
then Ball |[(- 1),0 ]|,ra meets V by A260, PRE_TOPC:def 13;
then consider u being set such that
A264: u in Ball |[(- 1),0 ]|,ra and
A265: u in V by XBOOLE_0:3;
|[1,0 ]| in Cl V by A14, A263, XBOOLE_0:def 4;
then Ball |[1,0 ]|,rb meets V by A261, PRE_TOPC:def 13;
then consider v being set such that
A266: v in Ball |[1,0 ]|,rb and
A267: v in V by XBOOLE_0:3;
reconsider u = u, v = v as Point of (TOP-REAL 2) by A264, A266;
A268: the carrier of (T2C | VP) = VP by PRE_TOPC:29;
reconsider u1 = u, v1 = v as Point of (T2C | VP) by A231, A265, A267, PRE_TOPC:29;
T2C | VP is arcwise_connected by A232, Th69;
then A269: u1,v1 are_connected by BORSUK_2:def 3;
then consider fuv being Function of I[01] ,(T2C | VP) such that
A270: ( fuv is continuous & fuv . 0 = u1 & fuv . 1 = v1 ) by BORSUK_2:def 1;
A271: T2C | VP = (TOP-REAL 2) | V by A231, GOBOARD9:4;
fuv is Path of u1,v1 by A269, A270, BORSUK_2:def 2;
then reconsider uv = fuv as Path of u,v by A269, A271, TOPALG_2:1;
A272: rng fuv c= the carrier of (T2C | VP) ;
then A273: rng uv misses rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A231, A246, A268, 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
A274: ( rng fau = LSeg |[(- 1),0 ]|,u & 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
A275: ( rng fvb = LSeg v,|[1,0 ]| & vb = fvb ) by Th43;
set AB = (au + uv) + vb;
A276: 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 A264, JORDAN1:def 1;
then A277: LSeg |[(- 1),0 ]|,u misses rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A254, XBOOLE_1:63;
|[1,0 ]| in Ball |[1,0 ]|,rb by Th16;
then LSeg v,|[1,0 ]| c= Ball |[1,0 ]|,rb by A266, JORDAN1:def 1;
then LSeg v,|[1,0 ]| misses rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A259, XBOOLE_1:63;
then A278: rng ((au + uv) + vb) misses rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) by A273, A274, A275, A276, A277, XBOOLE_1:114;
A279: |[(- 1),0 ]|,|[1,0 ]| are_connected by BORSUK_2:def 3;
A280: V c= closed_inside_of_rectangle (- 1),1,(- 3),3 by A1, A229, Th93;
then A281: LSeg |[(- 1),0 ]|,u c= closed_inside_of_rectangle (- 1),1,(- 3),3 by A11, A14, A265, JORDAN1:def 1;
A282: LSeg v,|[1,0 ]| c= closed_inside_of_rectangle (- 1),1,(- 3),3 by A11, A14, A267, A280, JORDAN1:def 1;
rng uv c= closed_inside_of_rectangle (- 1),1,(- 3),3 by A231, A268, A272, A280, XBOOLE_1:1;
then (LSeg |[(- 1),0 ]|,u) \/ (rng uv) c= closed_inside_of_rectangle (- 1),1,(- 3),3 by A281, XBOOLE_1:8;
then rng ((au + uv) + vb) c= the carrier of (Trectangle (- 1),1,(- 3),3) by A76, A274, A275, A276, A282, XBOOLE_1:8;
then reconsider h = (au + uv) + vb as Path of AR,BR by A279, Th29;
A283: |[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 A78, A79, XBOOLE_1:8;
then A284: ((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 A75, XBOOLE_1:8;
rng Pkj c= closed_inside_of_rectangle (- 1),1,(- 3),3 by A11, A45, XBOOLE_1:1;
then A285: (((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 A284, XBOOLE_1:8;
LSeg (LMP C),|[0 ,(- 3)]| c= closed_inside_of_rectangle (- 1),1,(- 3),3 by A11, A28, Lm61, Lm65, JORDAN1:def 1;
then rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) c= the carrier of (Trectangle (- 1),1,(- 3),3) by A76, A77, A234, A235, A236, A285, XBOOLE_1:8;
then reconsider v = (((Pcm + Pml) + Plk) + Pkj) + Pjd as Path of CR,DR by A283, Th29;
consider s, t being Point of I[01] such that
A286: h . s = v . t by Lm18, Lm19, Lm23, Lm25, JGRAPH_8:6;
( dom h = the carrier of I[01] & dom v = the carrier of I[01] ) by FUNCT_2:def 1;
then ( h . s in rng ((au + uv) + vb) & v . t in rng ((((Pcm + Pml) + Plk) + Pkj) + Pjd) ) by FUNCT_1:def 5;
hence contradiction by A278, A286, XBOOLE_0:3; :: thesis: verum