let n be Nat; :: thesis: for C being Simple_closed_curve
for i being 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 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 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 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 Lower_Arc C
set r = ((Gauge (C,n)) * (i,2)) `1 ;
4 <= len (Gauge (C,n)) by JORDAN8:10;
then A3: 1 + 1 <= len (Gauge (C,n)) by XXREAL_0:2;
then 1 <= (len (Gauge (C,n))) - 1 by XREAL_1:19;
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:16;
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:16;
A9: ((Gauge (C,n)) * (i,2)) `1 = ((Gauge (C,n)) * (i,1)) `1 by A1, A2, A5, A3, GOBOARD5:2
.= ((Gauge (C,n)) * (i,((len (Gauge (C,n))) -' 1))) `1 by A1, A2, A5, A4, A7, GOBOARD5:2 ;
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:13;
then A10: W-bound C <= ((Gauge (C,n)) * (i,2)) `1 by A3, JORDAN8:11;
i + 1 <= len (Gauge (C,n)) by A2, NAT_1:13;
then i <= (len (Gauge (C,n))) - 1 by XREAL_1:19;
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:13;
then A11: ((Gauge (C,n)) * (i,2)) `1 <= E-bound C by A4, JORDAN8:12, 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:53
.= |[(((Gauge (C,n)) * (i,((len (Gauge (C,n))) -' 1))) `1),(N-bound C)]| by A1, A2, JORDAN8:14 ;
(Gauge (C,n)) * (i,2) = |[(((Gauge (C,n)) * (i,2)) `1),(((Gauge (C,n)) * (i,2)) `2)]| by EUCLID:53
.= |[(((Gauge (C,n)) * (i,2)) `1),(S-bound C)]| by A1, A2, JORDAN8:13 ;
then LSeg (((Gauge (C,n)) * (i,2)),((Gauge (C,n)) * (i,((len (Gauge (C,n))) -' 1)))) meets Lower_Arc C by A12, A9, A10, A11, JORDAN6:70;
hence LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,(len (Gauge (C,n)))))) meets Lower_Arc C by A6, A8, TOPREAL1:6, XBOOLE_1:63; :: thesis: verum