let i, j, k be Element of NAT ; :: thesis: for C being being_simple_closed_curve Subset of (TOP-REAL 2) st i > 0 & 1 <= j & j <= width (Gauge C,i) & k <= j & 1 <= k & k <= width (Gauge 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))) = {((Gauge C,i) * (Center (Gauge C,i)),j)} & (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)} holds
LSeg ((Gauge C,i) * (Center (Gauge C,i)),j),((Gauge C,i) * (Center (Gauge C,i)),k) c= Cl (RightComp (Cage C,i))
let C be being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis: ( i > 0 & 1 <= j & j <= width (Gauge C,i) & k <= j & 1 <= k & k <= width (Gauge 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))) = {((Gauge C,i) * (Center (Gauge C,i)),j)} & (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)} implies LSeg ((Gauge C,i) * (Center (Gauge C,i)),j),((Gauge C,i) * (Center (Gauge C,i)),k) c= Cl (RightComp (Cage C,i)) )
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: LSeg ((Gauge C,i) * (Center (Gauge C,i)),j),((Gauge C,i) * (Center (Gauge C,i)),k) c= Cl (RightComp (Cage C,i))
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:17;
then A11: 1 < Center (Gauge C,i) by JORDAN1H:58, XXREAL_0:2;
A12: Center (Gauge C,i) < len (Gauge C,i) by A10, JORDAN1H:58;
then A13: [(Center (Gauge C,i)),j] in Indices (Gauge C,i) by A2, A3, A11, MATRIX_1:37;
(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:63;
A15: [(Center (Gauge C,i)),k] in Indices (Gauge C,i) by A5, A6, A11, A12, MATRIX_1:37;
(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:64;
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:32;
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:65
.= ((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:41 ;
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:43;
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:76, 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:65;
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:41;
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;
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, GOBOARD9:6, JORDAN1:52;
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:8; :: thesis: verum