for C being Simple_closed_curve
for i, j, k, n being Nat st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds
i < len (Gauge (C,n))