:: deftheorem defines SpanStart JORDAN14:def 1 :
for C being Simple_closed_curve
for n being Nat holds SpanStart (C,n) = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n)));