theorem Th10:
for
i,
j,
k,
m being
Nat for
C being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st
m > k &
[i,j] in Indices (Gauge (C,k)) &
[(i + 1),j] in Indices (Gauge (C,k)) holds
dist (
((Gauge (C,m)) * (i,j)),
((Gauge (C,m)) * ((i + 1),j)))
< dist (
((Gauge (C,k)) * (i,j)),
((Gauge (C,k)) * ((i + 1),j)))