let j, m, n be Nat; :: thesis: for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= m & m <= n & 1 <= j & j <= width (Gauge (E,n)) holds
LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,n)) * ((Center (Gauge (E,n))),j))) c= LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m))))))
let E be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( 1 <= m & m <= n & 1 <= j & j <= width (Gauge (E,n)) implies LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,n)) * ((Center (Gauge (E,n))),j))) c= LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m)))))) )
set a = N-bound E;
set s = S-bound E;
set w = W-bound E;
set e = E-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 that
A1: 1 <= m and
A2: m <= n and
A3: 1 <= j and
A4: j <= width (Gauge (E,n)) ; :: thesis: LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,n)) * ((Center (Gauge (E,n))),j))) c= LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m))))))
A5: ( 1 <= Center (Gauge (E,m)) & Center (Gauge (E,m)) <= len (Gauge (E,m)) ) by Lm3;
A6: ( 1 <= Center (Gauge (E,n)) & Center (Gauge (E,n)) <= len (Gauge (E,n)) ) by Lm3;
then A7: ((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 A2, A5, Th40;
len (Gauge (E,n)) = width (Gauge (E,n)) by JORDAN8:def 1;
then ((Gauge (E,n)) * ((Center (Gauge (E,n))),j)) `2 <= ((Gauge (E,n)) * ((Center (Gauge (E,n))),(len (Gauge (E,n))))) `2 by A3, A4, A6, SPRECT_3:12;
then A8: ((Gauge (E,n)) * ((Center (Gauge (E,n))),j)) `2 <= ((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m))))) `2 by A7, XXREAL_0:2;
A9: 0 < (N-bound E) - (S-bound E) by SPRECT_1:32, XREAL_1:50;
then A10: (S-bound E) - (((N-bound E) - (S-bound E)) / (2 |^ m)) <= (S-bound E) - 0 by XREAL_1:13;
A11: 1 <= len (Gauge (E,m)) by GOBRD11:34;
then [(Center (Gauge (E,m))),1] in Indices (Gauge (E,m)) by Lm4;
then A12: ((Gauge (E,m)) * ((Center (Gauge (E,m))),1)) `2 = (S-bound E) - (((N-bound E) - (S-bound E)) / (2 |^ m)) by Lm11;
A13: ((N-bound E) - (S-bound E)) / (2 |^ n) <= ((N-bound E) - (S-bound E)) / (2 |^ m) by A2, A9, Lm7;
A14: len (Gauge (E,n)) = width (Gauge (E,n)) by JORDAN8:def 1;
then A15: [(Center (Gauge (E,n))),j] in Indices (Gauge (E,n)) by A3, A4, Lm4;
then A16: ((Gauge (E,n)) * ((Center (Gauge (E,n))),j)) `2 = |[((W-bound E) + ((((E-bound E) - (W-bound E)) / (2 |^ n)) * ((Center (Gauge (E,n))) - 2))),((S-bound E) + ((((N-bound E) - (S-bound E)) / (2 |^ n)) * (j - 2)))]| `2 by JORDAN8:def 1
.= (S-bound E) + ((((N-bound E) - (S-bound E)) / (2 |^ n)) * (j - 2)) by EUCLID:52 ;

A17: now :: thesis: ((Gauge (E,m)) * ((Center (Gauge (E,m))),1)) `2 <= ((Gauge (E,n)) * ((Center (Gauge (E,n))),j)) `2

per cases ( j = 1 or j > 1 ) by A3, XXREAL_0:1;

suppose j = 1 ; :: thesis: ((Gauge (E,m)) * ((Center (Gauge (E,m))),1)) `2 <= ((Gauge (E,n)) * ((Center (Gauge (E,n))),j)) `2

then ((Gauge (E,n)) * ((Center (Gauge (E,n))),j)) `2 = (S-bound E) - (((N-bound E) - (S-bound E)) / (2 |^ n)) by A15, Lm11;
hence ((Gauge (E,m)) * ((Center (Gauge (E,m))),1)) `2 <= ((Gauge (E,n)) * ((Center (Gauge (E,n))),j)) `2 by A13, A12, XREAL_1:13; :: thesis: verum

end;

suppose j > 1 ; :: thesis: ((Gauge (E,m)) * ((Center (Gauge (E,m))),1)) `2 <= ((Gauge (E,n)) * ((Center (Gauge (E,n))),j)) `2

then j >= 1 + 1 by NAT_1:13;
then j - 2 >= 2 - 2 by XREAL_1:9;
then (S-bound E) + 0 <= (S-bound E) + ((((N-bound E) - (S-bound E)) / (2 |^ n)) * (j - 2)) by A9, XREAL_1:6;
hence ((Gauge (E,m)) * ((Center (Gauge (E,m))),1)) `2 <= ((Gauge (E,n)) * ((Center (Gauge (E,n))),j)) `2 by A12, A16, A10, XXREAL_0:2; :: thesis: verum

end;

end;

end;

len (Gauge (E,m)) = width (Gauge (E,m)) by JORDAN8:def 1;
then A18: ((Gauge (E,m)) * ((Center (Gauge (E,m))),1)) `2 <= ((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m))))) `2 by A11, A5, SPRECT_3:12;
((Gauge (E,m)) * ((Center (Gauge (E,m))),1)) `1 = ((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m))))) `1 by A1, A11, Th36;
then A19: (Gauge (E,m)) * ((Center (Gauge (E,m))),1) in LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m)))))) by A18, GOBOARD7:7;
( ((Gauge (E,m)) * ((Center (Gauge (E,m))),1)) `1 = ((Gauge (E,n)) * ((Center (Gauge (E,n))),j)) `1 & ((Gauge (E,n)) * ((Center (Gauge (E,n))),j)) `1 = ((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m))))) `1 ) by A1, A2, A3, A4, A11, A14, Th36;
then (Gauge (E,n)) * ((Center (Gauge (E,n))),j) in LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m)))))) by A17, A8, GOBOARD7:7;
hence LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,n)) * ((Center (Gauge (E,n))),j))) c= LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m)))))) by A19, TOPREAL1:6; :: thesis: verum