for n being Nat
for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
X-SpanStart (C,n) = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2