let n be Nat; :: thesis: for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
( 1 < Y-SpanStart (C,n) & Y-SpanStart (C,n) <= width (Gauge (C,n)) )
let C be being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis: ( n is_sufficiently_large_for C implies ( 1 < Y-SpanStart (C,n) & Y-SpanStart (C,n) <= width (Gauge (C,n)) ) )
assume A1: n is_sufficiently_large_for C ; :: thesis: ( 1 < Y-SpanStart (C,n) & Y-SpanStart (C,n) <= width (Gauge (C,n)) )
thus 1 < Y-SpanStart (C,n) :: thesis: Y-SpanStart (C,n) <= width (Gauge (C,n))

proof

A2: (X-SpanStart (C,n)) -' 1 <= len (Gauge (C,n)) by JORDAN1H:50;
assume A3: Y-SpanStart (C,n) <= 1 ; :: thesis: contradiction

per cases ( Y-SpanStart (C,n) = 0 or Y-SpanStart (C,n) = 1 ) by A3, NAT_1:25;

suppose A4: Y-SpanStart (C,n) = 0 ; :: thesis: contradiction

A5: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) c= UBD C by A2, JORDAN1A:49;
0 <= width (Gauge (C,n)) ;
then A6: not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) is empty by A2, JORDAN1A:24;
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) c= BDD C by A1, A4, Th6;
hence contradiction by A6, A5, JORDAN2C:24, XBOOLE_1:68; :: thesis: verum

end;

suppose Y-SpanStart (C,n) = 1 ; :: thesis: contradiction

then A7: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) c= BDD C by A1, Th6;
set i1 = X-SpanStart (C,n);
A8: (X-SpanStart (C,n)) -' 1 <= X-SpanStart (C,n) by NAT_D:44;
X-SpanStart (C,n) < len (Gauge (C,n)) by JORDAN1H:49;
then A9: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by A8, XXREAL_0:2;
BDD C c= C ` by JORDAN2C:25;
then A10: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) c= C ` by A7;
UBD C is_outside_component_of C by JORDAN2C:68;
then A11: UBD C is_a_component_of C ` by JORDAN2C:def 3;
A12: width (Gauge (C,n)) <> 0 by MATRIX_0:def 10;
then A13: 0 + 1 <= width (Gauge (C,n)) by NAT_1:14;
then A14: not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) is empty by A2, JORDAN1A:24;
1 <= (X-SpanStart (C,n)) -' 1 by JORDAN1H:50;
then (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0)) /\ (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(0 + 1))) = LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(0 + 1))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(0 + 1)))) by A12, A9, GOBOARD5:26;
then A15: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) meets cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(0 + 1)) ;
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) c= UBD C by A2, JORDAN1A:49;
then cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) c= UBD C by A13, A9, A15, A11, A10, GOBOARD9:4, JORDAN1A:25;
hence contradiction by A7, A14, JORDAN2C:24, XBOOLE_1:68; :: thesis: verum

end;

end;

end;

thus Y-SpanStart (C,n) <= width (Gauge (C,n)) by A1, Def3; :: thesis: verum