let C be Simple_closed_curve; :: thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
SpanStart C,n in BDD C
let n be Element of NAT ; :: thesis: ( n is_sufficiently_large_for C implies SpanStart C,n in BDD C )
A1: 1 <= (X-SpanStart C,n) -' 1 by JORDAN1H:59;
A2: (X-SpanStart C,n) -' 1 < len (Gauge C,n) by JORDAN1H:59;
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:23;
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, XBOOLE_1:1;
A7: 2 < X-SpanStart C,n by JORDAN1H:58;
(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:69;
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:237, XXREAL_0:2; :: thesis: verum