let n be Element of 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),(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),(Y-SpanStart C,n)] in Indices (Gauge C,n) )
A1: X-SpanStart C,n < len (Gauge C,n) by JORDAN1H:58;
1 + 1 < X-SpanStart C,n by JORDAN1H:58;
then A2: 1 < X-SpanStart C,n by NAT_1:13;
assume A3: n is_sufficiently_large_for C ; :: thesis: [(X-SpanStart C,n),(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),(Y-SpanStart C,n)] in Indices (Gauge C,n) by A2, A1, A4, MATRIX_1:37; :: thesis: verum