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) )
assume A1: n is_sufficiently_large_for C ; :: thesis: Y-SpanStart C,n < width (Gauge C,n)
A2: len (Span C,n) > 1 by GOBOARD7:36, XXREAL_0:2;
A3: [(X-SpanStart C,n),(Y-SpanStart C,n)] in Indices (Gauge C,n) by A1, JORDAN11:8;
(Span C,n) /. 1 = (Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n) by A1, JORDAN13:def 1;
hence Y-SpanStart C,n < width (Gauge C,n) by A1, A2, A3, Th26; :: thesis: verum