let k, m be 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