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