let C be Simple_closed_curve; :: thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
Y-SpanStart C,n < width (Gauge C,n)
let n be Element of NAT ; :: thesis: ( n is_sufficiently_large_for C implies Y-SpanStart C,n < width (Gauge C,n) )
A1: len (Span C,n) > 1 by GOBOARD7:36, XXREAL_0:2;
assume A2: n is_sufficiently_large_for C ; :: thesis: Y-SpanStart C,n < width (Gauge C,n)
then A3: (Span C,n) /. 1 = (Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n) by JORDAN13:def 1;
[(X-SpanStart C,n),(Y-SpanStart C,n)] in Indices (Gauge C,n) by A2, JORDAN11:8;
hence Y-SpanStart C,n < width (Gauge C,n) by A2, A1, A3, Th26; :: thesis: verum