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) * 1,2) < dist ((Gauge C,k) * 1,1),((Gauge C,k) * 1,2)
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) * 1,2) < dist ((Gauge C,k) * 1,1),((Gauge C,k) * 1,2) )
assume A1: m > k ; :: thesis: dist ((Gauge C,m) * 1,1),((Gauge C,m) * 1,2) < dist ((Gauge C,k) * 1,1),((Gauge C,k) * 1,2)
( [1,1] in Indices (Gauge C,k) & [1,(1 + 1)] in Indices (Gauge C,k) ) by Th5, Th6;
hence dist ((Gauge C,m) * 1,1),((Gauge C,m) * 1,2) < dist ((Gauge C,k) * 1,1),((Gauge C,k) * 1,2) by A1, Th8; :: thesis: verum