let n be Nat; 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); ( 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
; [((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; verum