let n be Nat; :: thesis: for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
[((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))] in Indices (Gauge (C,n))
let C be being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis: ( n is_sufficiently_large_for C implies [((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))] in Indices (Gauge (C,n)) )
A1: 1 <= (X-SpanStart (C,n)) -' 1 by JORDAN1H:50;
A2: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by JORDAN1H:50;
assume A3: n is_sufficiently_large_for C ; :: thesis: [((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))] in Indices (Gauge (C,n))
then A4: Y-SpanStart (C,n) <= width (Gauge (C,n)) by Th7;
1 < Y-SpanStart (C,n) by A3, Th7;
hence [((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))] in Indices (Gauge (C,n)) by A1, A2, A4, MATRIX_0:30; :: thesis: verum