let n be Element of NAT ; :: thesis: for C being Simple_closed_curve
for i being Element of NAT st 1 < i & i < len (Gauge C,n) holds
LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,(len (Gauge C,n))) meets Lower_Arc C
let C be Simple_closed_curve; :: thesis: for i being Element of NAT st 1 < i & i < len (Gauge C,n) holds
LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,(len (Gauge C,n))) meets Lower_Arc C
let i be Element of NAT ; :: thesis: ( 1 < i & i < len (Gauge C,n) implies LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,(len (Gauge C,n))) meets Lower_Arc C )
assume A1: ( 1 < i & i < len (Gauge C,n) ) ; :: thesis: LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,(len (Gauge C,n))) meets Lower_Arc C
A2: (Gauge C,n) * i,2 = |[(((Gauge C,n) * i,2) `1 ),(((Gauge C,n) * i,2) `2 )]| by EUCLID:57
.= |[(((Gauge C,n) * i,2) `1 ),(S-bound C)]| by A1, JORDAN8:16 ;
A3: (Gauge C,n) * i,((len (Gauge C,n)) -' 1) = |[(((Gauge C,n) * i,((len (Gauge C,n)) -' 1)) `1 ),(((Gauge C,n) * i,((len (Gauge C,n)) -' 1)) `2 )]| by EUCLID:57
.= |[(((Gauge C,n) * i,((len (Gauge C,n)) -' 1)) `1 ),(N-bound C)]| by A1, JORDAN8:17 ;
set r = ((Gauge C,n) * i,2) `1 ;
A4: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
4 <= len (Gauge C,n) by JORDAN8:13;
then A5: 1 + 1 <= len (Gauge C,n) by XXREAL_0:2;
then 1 <= (len (Gauge C,n)) - 1 by XREAL_1:21;
then A6: 1 <= (len (Gauge C,n)) -' 1 by XREAL_0:def 2;
A7: (len (Gauge C,n)) -' 1 <= len (Gauge C,n) by NAT_D:35;
A8: ((Gauge C,n) * i,2) `1 = ((Gauge C,n) * i,1) `1 by A1, A4, A5, GOBOARD5:3
.= ((Gauge C,n) * i,((len (Gauge C,n)) -' 1)) `1 by A1, A4, A6, A7, GOBOARD5:3 ;
1 + 1 <= i by A1, NAT_1:13;
then ((Gauge C,n) * 2,2) `1 <= ((Gauge C,n) * i,2) `1 by A1, A4, A5, SPRECT_3:25;
then A9: W-bound C <= ((Gauge C,n) * i,2) `1 by A5, JORDAN8:14;
i + 1 <= len (Gauge C,n) by A1, NAT_1:13;
then i <= (len (Gauge C,n)) - 1 by XREAL_1:21;
then i <= (len (Gauge C,n)) -' 1 by XREAL_0:def 2;
then ((Gauge C,n) * i,2) `1 <= ((Gauge C,n) * ((len (Gauge C,n)) -' 1),((len (Gauge C,n)) -' 1)) `1 by A1, A4, A6, A7, A8, SPRECT_3:25;
then ((Gauge C,n) * i,2) `1 <= E-bound C by A6, NAT_D:35, JORDAN8:15;
then A10: LSeg ((Gauge C,n) * i,2),((Gauge C,n) * i,((len (Gauge C,n)) -' 1)) meets Lower_Arc C by A2, A3, A8, A9, JORDAN6:85;
A11: (Gauge C,n) * i,2 in LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,(len (Gauge C,n))) by A1, A4, A5, JORDAN1A:37;
(Gauge C,n) * i,((len (Gauge C,n)) -' 1) in LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,(len (Gauge C,n))) by A1, A4, A6, A7, JORDAN1A:37;
hence LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,(len (Gauge C,n))) meets Lower_Arc C by A10, A11, TOPREAL1:12, XBOOLE_1:63; :: thesis: verum