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 )
assume A1: n is_sufficiently_large_for C ; :: thesis: SpanStart C,n in BDD C
then A2: cell (Gauge C,n),((X-SpanStart C,n) -' 1),(Y-SpanStart C,n) c= BDD C by JORDAN11:6;
A3: ( 1 <= (X-SpanStart C,n) -' 1 & (X-SpanStart C,n) -' 1 < len (Gauge C,n) ) by JORDAN1H:59;
A4: ( 1 < Y-SpanStart C,n & Y-SpanStart C,n <= width (Gauge C,n) ) by A1, JORDAN11:7;
A5: 2 < X-SpanStart C,n by JORDAN1H:58;
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 A3, A4, 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 A2, XBOOLE_1:1;
(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 A5, XREAL_1:237, XXREAL_0:2; :: thesis: verum