let n be Element of NAT ; :: thesis: for C being Simple_closed_curve
for i, j, k being Element of NAT st 1 < i & i < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & n > 0 & (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Lower_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,k)} & (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Upper_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,j)} holds
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets Upper_Arc C
let C be Simple_closed_curve; :: thesis: for i, j, k being Element of NAT st 1 < i & i < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & n > 0 & (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Lower_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,k)} & (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Upper_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,j)} holds
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets Upper_Arc C
let i, j, k be Element of NAT ; :: thesis: ( 1 < i & i < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & n > 0 & (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Lower_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,k)} & (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Upper_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,j)} implies LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets Upper_Arc C )
assume that
A1: 1 < i and
A2: i < len (Gauge C,n) and
A3: 1 <= j and
A4: j <= k and
A5: k <= width (Gauge C,n) and
A6: n > 0 and
A7: (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Lower_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,k)} and
A8: (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Upper_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,j)} ; :: thesis: LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets Upper_Arc C
A9: L~ (Lower_Seq C,n) = Lower_Arc (L~ (Cage C,n)) by A6, JORDAN1G:64;
L~ (Upper_Seq C,n) = Upper_Arc (L~ (Cage C,n)) by A6, JORDAN1G:63;
hence LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets Upper_Arc C by A1, A2, A3, A4, A5, A7, A8, A9, Th13; :: thesis: verum