let C be Simple_closed_curve; :: thesis: for n being Nat st n is_sufficiently_large_for C holds
Y-SpanStart (C,n) < width (Gauge (C,n))
let n be 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:34, 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, Th25; :: thesis: verum