let m, n be Element of NAT ; :: thesis:
let E be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis:
set a = N-bound E;
set s = S-bound E;
set G = Gauge (E,n);
set M = Gauge (E,m);
set sn = Center (Gauge (E,n));
set sm = Center (Gauge (E,m));
assume A1: 1 <= m ; :: thesis:
A2: 1 <= len (Gauge (E,m)) by GOBRD11:34;
then [(Center (Gauge (E,m))),1] in Indices (Gauge (E,m)) by Lm4;
then A3: ((Gauge (E,m)) * ((Center (Gauge (E,m))),1)) `2 = (S-bound E) - (((N-bound E) - (S-bound E)) / (2 |^ m)) by Lm11;
[(Center (Gauge (E,m))),(len (Gauge (E,m)))] in Indices (Gauge (E,m)) by A2, Lm4;
then A4: ((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m))))) `2 = (N-bound E) + (((N-bound E) - (S-bound E)) / (2 |^ m)) by Lm13;
A5: Center (Gauge (E,n)) <= len (Gauge (E,n)) by Lm3;
A6: 1 <= len (Gauge (E,n)) by GOBRD11:34;
assume A7: m <= n ; :: thesis:
then A8: ( ((Gauge (E,m)) * ((Center (Gauge (E,m))),1)) `1 = ((Gauge (E,n)) * ((Center (Gauge (E,n))),(len (Gauge (E,n))))) `1 & ((Gauge (E,n)) * ((Center (Gauge (E,n))),(len (Gauge (E,n))))) `1 = ((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m))))) `1 ) by A1, A6, A2, Th57;
0 < (N-bound E) - (S-bound E) by SPRECT_1:32, XREAL_1:50;
then A9: ((N-bound E) - (S-bound E)) / (2 |^ n) <= ((N-bound E) - (S-bound E)) / (2 |^ m) by A7, Lm7;
( len (Gauge (E,n)) = width (Gauge (E,n)) & 1 <= Center (Gauge (E,n)) ) by Lm3, JORDAN8:def 1;
then A10: ((Gauge (E,n)) * ((Center (Gauge (E,n))),1)) `2 <= ((Gauge (E,n)) * ((Center (Gauge (E,n))),(len (Gauge (E,n))))) `2 by A6, A5, SPRECT_3:12;
[(Center (Gauge (E,n))),(len (Gauge (E,n)))] in Indices (Gauge (E,n)) by A6, Lm4;
then ((Gauge (E,n)) * ((Center (Gauge (E,n))),(len (Gauge (E,n))))) `2 = (N-bound E) + (((N-bound E) - (S-bound E)) / (2 |^ n)) by Lm13;
then A11: ((Gauge (E,n)) * ((Center (Gauge (E,n))),(len (Gauge (E,n))))) `2 <= ((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m))))) `2 by A9, A4, XREAL_1:7;
then A12: ((Gauge (E,n)) * ((Center (Gauge (E,n))),1)) `2 <= ((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m))))) `2 by A10, XXREAL_0:2;
[(Center (Gauge (E,n))),1] in Indices (Gauge (E,n)) by A6, Lm4;
then ((Gauge (E,n)) * ((Center (Gauge (E,n))),1)) `2 = (S-bound E) - (((N-bound E) - (S-bound E)) / (2 |^ n)) by Lm11;
then A13: ((Gauge (E,m)) * ((Center (Gauge (E,m))),1)) `2 <= ((Gauge (E,n)) * ((Center (Gauge (E,n))),1)) `2 by A9, A3, XREAL_1:13;
then ((Gauge (E,m)) * ((Center (Gauge (E,m))),1)) `2 <= ((Gauge (E,n)) * ((Center (Gauge (E,n))),(len (Gauge (E,n))))) `2 by A10, XXREAL_0:2;
then A14: (Gauge (E,n)) * ((Center (Gauge (E,n))),(len (Gauge (E,n)))) in LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m)))))) by A11, A8, GOBOARD7:7;
( ((Gauge (E,m)) * ((Center (Gauge (E,m))),1)) `1 = ((Gauge (E,n)) * ((Center (Gauge (E,n))),1)) `1 & ((Gauge (E,n)) * ((Center (Gauge (E,n))),1)) `1 = ((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m))))) `1 ) by A1, A7, A6, A2, Th57;
then (Gauge (E,n)) * ((Center (Gauge (E,n))),1) in LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m)))))) by A13, A12, GOBOARD7:7;
hence LSeg (((Gauge (E,n)) * ((Center (Gauge (E,n))),1)),((Gauge (E,n)) * ((Center (Gauge (E,n))),(len (Gauge (E,n)))))) c= LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m)))))) by A14, TOPREAL1:6; :: thesis: