let C be Simple_closed_curve; :: thesis: for n being Nat st n is_sufficiently_large_for C holds
SpanStart (C,n) in BDD C
let n be Nat; :: thesis: ( n is_sufficiently_large_for C implies SpanStart (C,n) in BDD C )
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 ; :: thesis: SpanStart (C,n) in BDD C
then A4: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) c= BDD C by JORDAN11:6;
A5: Y-SpanStart (C,n) <= width (Gauge (C,n)) by A3, JORDAN11:7;
1 < Y-SpanStart (C,n) by A3, JORDAN11:7;
then LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n)))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(Y-SpanStart (C,n))))) c= cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) by A1, A2, A5, GOBOARD5:22;
then A6: LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n)))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(Y-SpanStart (C,n))))) c= BDD C by A4;
A7: 2 < X-SpanStart (C,n) by JORDAN1H:49;
(Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(Y-SpanStart (C,n))) in LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n)))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(Y-SpanStart (C,n))))) by RLTOPSP1:68;
then (Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(Y-SpanStart (C,n))) in BDD C by A6;
hence SpanStart (C,n) in BDD C by A7, XREAL_1:235, XXREAL_0:2; :: thesis: verum