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) c= BDD 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) c= BDD C )
assume A1: n is_sufficiently_large_for C ; :: thesis: cell (Gauge C,n),((X-SpanStart C,n) -' 1),(Y-SpanStart C,n) c= BDD C
then Y-SpanStart C,n <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by Th5;
hence cell (Gauge C,n),((X-SpanStart C,n) -' 1),(Y-SpanStart C,n) c= BDD C by A1, Def3; :: thesis: verum