let C be Simple_closed_curve; :: thesis: for i, j, k, n being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k <= len (Span C,n) & [i,j] in Indices (Gauge C,n) & (Span C,n) /. k = (Gauge C,n) * i,j holds
j < width (Gauge C,n)
let i, j, k, n be Element of NAT ; :: thesis: ( n is_sufficiently_large_for C & 1 <= k & k <= len (Span C,n) & [i,j] in Indices (Gauge C,n) & (Span C,n) /. k = (Gauge C,n) * i,j implies j < width (Gauge C,n) )
assume that
A1: n is_sufficiently_large_for C and
A2: ( 1 <= k & k <= len (Span C,n) ) and
A3: [i,j] in Indices (Gauge C,n) and
A4: (Span C,n) /. k = (Gauge C,n) * i,j ; :: thesis: j < width (Gauge C,n)
A5: ( 1 <= i & i <= len (Gauge C,n) & 1 <= j & j <= width (Gauge C,n) ) by A3, MATRIX_1:39;
A6: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
A7: ((Gauge C,n) * i,((len (Gauge C,n)) -' 1)) `2 = N-bound C by A5, JORDAN8:17;
SpanStart C,n in BDD C by A1, Th7;
then A8: N-bound C >= N-bound (BDD C) by JORDAN1C:21;
A9: BDD C is Bounded by JORDAN2C:114;
then A10: Cl (BDD C) is compact by TOPREAL6:71, TOPREAL6:88;
A11: BDD C c= Cl (BDD C) by PRE_TOPC:48;
L~ (Span C,n) c= BDD C by A1, Th22;
then A12: N-bound (L~ (Span C,n)) <= N-bound (Cl (BDD C)) by A10, A11, PSCOMP_1:129, XBOOLE_1:1;
SpanStart C,n in BDD C by A1, Th7;
then A13: N-bound (BDD C) = N-bound (Cl (BDD C)) by A9, TOPREAL6:96;
A14: len (Gauge C,n) >= 4 by JORDAN8:13;
then len (Gauge C,n) >= 0 + 1 by XXREAL_0:2;
then A15: (len (Gauge C,n)) - 1 >= 0 by XREAL_1:21;
len (Gauge C,n) >= 1 + 1 by A14, XXREAL_0:2;
then (len (Gauge C,n)) - 1 >= 1 by XREAL_1:21;
then A16: (len (Gauge C,n)) -' 1 >= 1 by A15, XREAL_0:def 2;
A17: len (Span C,n) > 4 by GOBOARD7:36;
k in dom (Span C,n) by A2, FINSEQ_3:27;
then (Span C,n) /. k in L~ (Span C,n) by A17, GOBOARD1:16, XXREAL_0:2;
then N-bound (L~ (Span C,n)) >= ((Gauge C,n) * i,j) `2 by A4, PSCOMP_1:71;
then N-bound (BDD C) >= ((Gauge C,n) * i,j) `2 by A12, A13, XXREAL_0:2;
then ((Gauge C,n) * i,((len (Gauge C,n)) -' 1)) `2 >= ((Gauge C,n) * i,j) `2 by A7, A8, XXREAL_0:2;
then j <= (len (Gauge C,n)) -' 1 by A5, A16, GOBOARD5:5;
then j < ((len (Gauge C,n)) -' 1) + 1 by NAT_1:13;
hence j < width (Gauge C,n) by A6, A14, XREAL_1:237, XXREAL_0:2; :: thesis: verum