let i, j, k be Nat; :: thesis:
let C be being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis:
assume that
A1: i > 0 and
A2: 1 <= j and
A3: j <= width (Gauge (C,i)) and
A4: k <= j and
A5: 1 <= k and
A6: k <= width (Gauge (C,i)) and
A7: (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Upper_Arc (L~ (Cage (C,i)))) = {((Gauge (C,i)) * ((Center (Gauge (C,i))),j))} and
A8: (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))) = {((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} ; :: thesis:
set p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j);
set q = (Gauge (C,i)) * ((Center (Gauge (C,i))),k);
set S = RightComp (Cage (C,i));
A9: {((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} c= Lower_Arc (L~ (Cage (C,i))) by A8, XBOOLE_1:17;
A10: X-SpanStart (C,i) = Center (Gauge (C,i)) by JORDAN1B:16;
then A11: 1 < Center (Gauge (C,i)) by JORDAN1H:49, XXREAL_0:2;
A12: Center (Gauge (C,i)) < len (Gauge (C,i)) by A10, JORDAN1H:49;
then A13: [(Center (Gauge (C,i))),j] in Indices (Gauge (C,i)) by A2, A3, A11, MATRIX_0:30;
(Gauge (C,i)) * ((Center (Gauge (C,i))),j) in {((Gauge (C,i)) * ((Center (Gauge (C,i))),j))} by TARSKI:def 1;
then (Gauge (C,i)) * ((Center (Gauge (C,i))),j) in Upper_Arc (L~ (Cage (C,i))) by A7, XBOOLE_0:def 4;
then A14: (Gauge (C,i)) * ((Center (Gauge (C,i))),j) in L~ (Upper_Seq (C,i)) by A1, JORDAN1G:55;
A15: [(Center (Gauge (C,i))),k] in Indices (Gauge (C,i)) by A5, A6, A11, A12, MATRIX_0:30;
(Gauge (C,i)) * ((Center (Gauge (C,i))),k) in {((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} by TARSKI:def 1;
then (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Lower_Arc (L~ (Cage (C,i))) by A8, XBOOLE_0:def 4;
then (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in L~ (Lower_Seq (C,i)) by A1, JORDAN1G:56;
then j <> k by A2, A6, A11, A12, A14, JORDAN1J:57;
then A16: (Gauge (C,i)) * ((Center (Gauge (C,i))),j) <> (Gauge (C,i)) * ((Center (Gauge (C,i))),k) by A13, A15, JORDAN1H:26;
set A = (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) \ {((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))};
(LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Cage (C,i))) = (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ ((Upper_Arc (L~ (Cage (C,i)))) \/ (Lower_Arc (L~ (Cage (C,i))))) by JORDAN6:50
.= ((LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Upper_Arc (L~ (Cage (C,i))))) \/ ((LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i))))) by XBOOLE_1:23
.= {((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} by A7, A8, ENUMSET1:1 ;
then (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) \ {((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} misses L~ (Cage (C,i)) by XBOOLE_1:90;
then A17: (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) \ {((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} c= (L~ (Cage (C,i))) ` by SUBSET_1:23;
A18: C c= RightComp (Cage (C,i)) by JORDAN10:11;
LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),k)),((Gauge (C,i)) * ((Center (Gauge (C,i))),j))) meets Upper_Arc C by A1, A3, A4, A5, A7, A8, A11, A12, JORDAN1J:61;
then A19: LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),k)),((Gauge (C,i)) * ((Center (Gauge (C,i))),j))) meets C by JORDAN6:61, XBOOLE_1:63;
{((Gauge (C,i)) * ((Center (Gauge (C,i))),j))} c= Upper_Arc (L~ (Cage (C,i))) by A7, XBOOLE_1:17;
then {((Gauge (C,i)) * ((Center (Gauge (C,i))),j))} \/ {((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} c= (Upper_Arc (L~ (Cage (C,i)))) \/ (Lower_Arc (L~ (Cage (C,i)))) by A9, XBOOLE_1:13;
then {((Gauge (C,i)) * ((Center (Gauge (C,i))),j))} \/ {((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} c= L~ (Cage (C,i)) by JORDAN6:50;
then A20: {((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} c= L~ (Cage (C,i)) by ENUMSET1:1;
L~ (Cage (C,i)) misses C by JORDAN10:5;
then {((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} misses C by A20, XBOOLE_1:63;
then A21: (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) \ {((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} meets C by A19, XBOOLE_1:84;
A22: (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) \ {((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} is convex by JORDAN1:46;
RightComp (Cage (C,i)) is_a_component_of (L~ (Cage (C,i))) ` by GOBOARD9:def 2;
then (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) \ {((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} c= RightComp (Cage (C,i)) by A17, A21, A18, A22, GOBOARD9:4;
hence LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) c= Cl (RightComp (Cage (C,i))) by A16, JORDAN1H:3; :: thesis: