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);
X-SpanStart C,i = Center (Gauge C,i) by JORDAN1B:17;
then ( 2 <= Center (Gauge C,i) & Center (Gauge C,i) < len (Gauge C,i) ) by JORDAN1H:58;
then A9: ( 1 < Center (Gauge C,i) & Center (Gauge C,i) < len (Gauge C,i) ) by XXREAL_0:2;
(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 A10: (Gauge C,i) * (Center (Gauge C,i)),k in L~ (Lower_Seq C,i) by A1, JORDAN1G:64;
(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 (Gauge C,i) * (Center (Gauge C,i)),j in L~ (Upper_Seq C,i) by A1, JORDAN1G:63;
then A11: j <> k by A2, A6, A9, A10, JORDAN1J:57;
A12: [(Center (Gauge C,i)),j] in Indices (Gauge C,i) by A2, A3, A9, MATRIX_1:37;
[(Center (Gauge C,i)),k] in Indices (Gauge C,i) by A5, A6, A9, MATRIX_1:37;
then A13: (Gauge C,i) * (Center (Gauge C,i)),j <> (Gauge C,i) * (Center (Gauge C,i)),k by A11, A12, 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)};
A14: RightComp (Cage C,i) is_a_component_of (L~ (Cage C,i)) ` by GOBOARD9:def 2;
(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 A15: (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;
A16: 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, A9, JORDAN1J:61;
Upper_Arc C c= C by JORDAN6:76;
then A17: LSeg ((Gauge C,i) * (Center (Gauge C,i)),k),((Gauge C,i) * (Center (Gauge C,i)),j) meets C by A16, XBOOLE_1:63;
A18: {((Gauge C,i) * (Center (Gauge C,i)),j)} c= Upper_Arc (L~ (Cage C,i)) by A7, XBOOLE_1:17;
{((Gauge C,i) * (Center (Gauge C,i)),k)} c= Lower_Arc (L~ (Cage C,i)) by A8, 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 A18, 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 A19: {((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 A19, XBOOLE_1:63;
then A20: (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 A17, XBOOLE_1:84;
C c= RightComp (Cage C,i) by JORDAN10:11;
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 A14, A15, A20, 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 A13, JORDAN1H:8; :: thesis: verum