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 > 1
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 > 1 )
assume that
A1: n is_sufficiently_large_for C and
A2: 1 <= k and
A3: k <= len (Span C,n) and
A4: [i,j] in Indices (Gauge C,n) and
A5: (Span C,n) /. k = (Gauge C,n) * i,j ; :: thesis: j > 1
A6: len (Span C,n) > 4 by GOBOARD7:36;
SpanStart C,n in BDD C by A1, Th7;
then A7: S-bound C <= S-bound (BDD C) by JORDAN1C:20;
A8: i <= len (Gauge C,n) by A4, MATRIX_1:39;
k in dom (Span C,n) by A2, A3, FINSEQ_3:27;
then (Span C,n) /. k in L~ (Span C,n) by A6, GOBOARD1:16, XXREAL_0:2;
then A9: S-bound (L~ (Span C,n)) <= ((Gauge C,n) * i,j) `2 by A5, PSCOMP_1:71;
A10: BDD C c= Cl (BDD C) by PRE_TOPC:48;
A11: BDD C is Bounded by JORDAN2C:114;
then A12: Cl (BDD C) is compact by TOPREAL6:71, TOPREAL6:88;
SpanStart C,n in BDD C by A1, Th7;
then A13: S-bound (BDD C) = S-bound (Cl (BDD C)) by A11, TOPREAL6:97;
L~ (Span C,n) c= BDD C by A1, Th22;
then S-bound (L~ (Span C,n)) >= S-bound (Cl (BDD C)) by A12, A10, PSCOMP_1:131, XBOOLE_1:1;
then A14: S-bound (BDD C) <= ((Gauge C,n) * i,j) `2 by A13, A9, XXREAL_0:2;
len (Gauge C,n) >= 4 by JORDAN8:13;
then A15: len (Gauge C,n) >= 2 by XXREAL_0:2;
A16: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
A17: 1 <= i by A4, MATRIX_1:39;
then ((Gauge C,n) * i,2) `2 = S-bound C by A8, JORDAN8:16;
then A18: ((Gauge C,n) * i,2) `2 <= ((Gauge C,n) * i,j) `2 by A7, A14, XXREAL_0:2;
1 <= j by A4, MATRIX_1:39;
then j >= 1 + 1 by A17, A8, A16, A15, A18, GOBOARD5:5;
hence j > 1 by NAT_1:13; :: thesis: verum