let n be Element of NAT ; :: thesis: for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
cell (Gauge C,n),((X-SpanStart C,n) -' 1),(Y-SpanStart C,n) misses C
let C be being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis: ( n is_sufficiently_large_for C implies cell (Gauge C,n),((X-SpanStart C,n) -' 1),(Y-SpanStart C,n) misses C )
assume n is_sufficiently_large_for C ; :: thesis: cell (Gauge C,n),((X-SpanStart C,n) -' 1),(Y-SpanStart C,n) misses C
then cell (Gauge C,n),((X-SpanStart C,n) -' 1),(Y-SpanStart C,n) c= BDD C by Th6;
hence cell (Gauge C,n),((X-SpanStart C,n) -' 1),(Y-SpanStart C,n) misses C by JORDAN1A:15, XBOOLE_1:63; :: thesis: verum