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) & (Gauge C,n) * k,i in L~ (Upper_Seq C,n) & (Gauge C,n) * j,i in L~ (Lower_Seq 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) & (Gauge C,n) * k,i in L~ (Upper_Seq C,n) & (Gauge C,n) * j,i in L~ (Lower_Seq 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) & (Gauge C,n) * k,i in L~ (Upper_Seq C,n) & (Gauge C,n) * j,i in L~ (Lower_Seq C,n) implies LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i) meets Upper_Arc C )
assume that
A1: 1 < j and
A2: j <= k and
A3: k < len (Gauge C,n) and
A4: 1 <= i and
A5: i <= width (Gauge C,n) and
A6: (Gauge C,n) * k,i in L~ (Upper_Seq C,n) and
A7: (Gauge C,n) * j,i in L~ (Lower_Seq C,n) ; :: thesis: LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i) meets Upper_Arc C
consider j1, k1 being Element of NAT such that
A8: j <= j1 and
A9: j1 <= k1 and
A10: k1 <= k and
A11: (LSeg ((Gauge C,n) * j1,i),((Gauge C,n) * k1,i)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * j1,i)} and
A12: (LSeg ((Gauge C,n) * j1,i),((Gauge C,n) * k1,i)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * k1,i)} by A1, A2, A3, A4, A5, A6, A7, Th16;
A13: k1 < len (Gauge C,n) by A3, A10, XXREAL_0:2;
1 < j1 by A1, A8, XXREAL_0:2;
then LSeg ((Gauge C,n) * j1,i),((Gauge C,n) * k1,i) meets Upper_Arc C by A4, A5, A9, A11, A12, A13, Th31;
hence LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i) meets Upper_Arc C by A1, A3, A4, A5, A8, A9, A10, Th8, XBOOLE_1:63; :: thesis: verum