let n be Nat; 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); ( 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
; 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:7, XBOOLE_1:63; verum