for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for f being FinSequence of (TOP-REAL 2)
for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on Gauge (C,n) & not dist ((f /. k),(f /. (k + 1))) = ((N-bound C) - (S-bound C)) / (2 |^ n) holds
dist ((f /. k),(f /. (k + 1))) = ((E-bound C) - (W-bound C)) / (2 |^ n)