for C being Simple_closed_curve
for n, k being Nat st n is_sufficiently_large_for C & 1 <= k & k + 1 <= len (Span (C,n)) holds
( right_cell ((Span (C,n)),k,(Gauge (C,n))) misses C & left_cell ((Span (C,n)),k,(Gauge (C,n))) meets C )