let m, k be Element of NAT ; :: thesis: 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)
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( m > k implies dist ((Gauge C,m) * 1,1),((Gauge C,m) * 2,1) < dist ((Gauge C,k) * 1,1),((Gauge C,k) * 2,1) )
assume A1: m > k ; :: thesis: dist ((Gauge C,m) * 1,1),((Gauge C,m) * 2,1) < dist ((Gauge C,k) * 1,1),((Gauge C,k) * 2,1)
[(1 + 1),1] in Indices (Gauge C,k) by Th7;
hence dist ((Gauge C,m) * 1,1),((Gauge C,m) * 2,1) < dist ((Gauge C,k) * 1,1),((Gauge C,k) * 2,1) by A1, Th5, Th10; :: thesis: verum