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) -' 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) )
assume A1: n is_sufficiently_large_for C ; :: thesis: [((X-SpanStart C,n) -' 1),(Y-SpanStart C,n)] in Indices (Gauge C,n)
A2: ( 1 <= (X-SpanStart C,n) -' 1 & (X-SpanStart C,n) -' 1 < len (Gauge C,n) ) by JORDAN1H:59;
( 1 < Y-SpanStart C,n & Y-SpanStart C,n <= width (Gauge C,n) ) by A1, Th7;
hence [((X-SpanStart C,n) -' 1),(Y-SpanStart C,n)] in Indices (Gauge C,n) by A2, MATRIX_1:37; :: thesis: verum