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