theorem Th11: :: JORDAN22:11

for k, m being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k holds
dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1)))