for C being Simple_closed_curve
for n, k being Nat st n is_sufficiently_large_for C & Y-SpanStart (C,n) <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
(cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k)) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n)))