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 Upper_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 Upper_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 Upper_Arc C )
assume that
A1: 1 < i and
A2: i < len (Gauge C,n) ; :: thesis: LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,(len (Gauge C,n))) meets Upper_Arc C
set r = ((Gauge C,n) * i,2) `1 ;
4 <= len (Gauge C,n) by JORDAN8:13;
then A3: 1 + 1 <= len (Gauge C,n) by XXREAL_0:2;
then 1 <= (len (Gauge C,n)) - 1 by XREAL_1:21;
then A4: 1 <= (len (Gauge C,n)) -' 1 by XREAL_0:def 2;
A5: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
then A6: (Gauge C,n) * i,2 in LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,(len (Gauge C,n))) by A1, A2, A3, JORDAN1A:37;
A7: (len (Gauge C,n)) -' 1 <= len (Gauge C,n) by NAT_D:35;
then A8: (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, A2, A5, A4, JORDAN1A:37;
A9: ((Gauge C,n) * i,2) `1 = ((Gauge C,n) * i,1) `1 by A1, A2, A5, A3, GOBOARD5:3
.= ((Gauge C,n) * i,((len (Gauge C,n)) -' 1)) `1 by A1, A2, A5, A4, 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 A2, A5, A3, SPRECT_3:25;
then A10: W-bound C <= ((Gauge C,n) * i,2) `1 by A3, JORDAN8:14;
i + 1 <= len (Gauge C,n) by A2, 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, A5, A4, A7, A9, SPRECT_3:25;
then A11: ((Gauge C,n) * i,2) `1 <= E-bound C by A4, JORDAN8:15, NAT_D:35;
A12: (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, A2, JORDAN8:17 ;
(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, A2, JORDAN8:16 ;
then LSeg ((Gauge C,n) * i,2),((Gauge C,n) * i,((len (Gauge C,n)) -' 1)) meets Upper_Arc C by A12, A9, A10, A11, JORDAN6:84;
hence LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,(len (Gauge C,n))) meets Upper_Arc C by A6, A8, TOPREAL1:12, XBOOLE_1:63; :: thesis: verum