let C be Simple_closed_curve; ( |[(- 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
; 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); ( 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
; 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); ( 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 `)))
; ( 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 ;
TARSKI:def 3 ( 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 `
;
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 Jc
;
contradictionthen
q in Jc /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))
by A70, XBOOLE_0:def 4;
then A71:
(LMP Jc) `2 <= q `2
by A8, A9, JORDAN21:29;
q `2 <= (LMP Jc) `2
by A22, A44, A56, A57, A59, A67, JGRAPH_6:1;
then
(LMP Jc) `2 = q `2
by A71, XXREAL_0:1;
then
LMP Jc = q
by A12, A13, A22, 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;
verum end; suppose
q in Jd
;
contradictionthen 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;
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 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))}
;
contradictionthen
(
(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;
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
for V being Subset of (TOP-REAL 2) st V is_inside_component_of C holds
V = Uxproof
thus A89:
Ux is_a_component_of C `
by A10, A52;
JORDAN2C:def 2 Ux is bounded
assume
not
Ux is
bounded
;
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
;
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;
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
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
;
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;
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 ;
TARSKI:def 3 ( 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)}
;
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;
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
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
;
contradictionper 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)]|)
;
contradictionconsider 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;
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)]|)
;
contradictionconsider 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;
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)]|)
;
contradictionconsider 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;
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]|)
;
contradictionconsider 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;
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
;
contradictionper 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]|)
;
contradictionconsider 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;
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]|)
;
contradictionconsider 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;
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]|)
;
contradictionconsider 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;
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]|)
;
contradictionconsider 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;
verum end; end; end; end;
end;
let V be Subset of (TOP-REAL 2); ( V is_inside_component_of C implies V = Ux )
assume A285:
V is_inside_component_of C
; V = Ux
assume A286:
V <> Ux
; 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 ;
TARSKI:def 3 ( 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))}
;
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;
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
;
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;
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; verum