:: deftheorem defines X-SpanStart JORDAN1H:def 2 :
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds X-SpanStart (C,n) = (2 |^ (n -' 1)) + 2;