theorem Th9: :: GOBRD14:9

for i, j, n being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st [i,j] in Indices (Gauge (C,n)) & [i,(j + 1)] in Indices (Gauge (C,n)) holds
dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,(j + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n)