let m, n, j be Element of 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: 0 < (N-bound E) - (S-bound E) by SPRECT_1:34, XREAL_1:52;
then A6: ((N-bound E) - (S-bound E)) / (2 |^ n) <= ((N-bound E) - (S-bound E)) / (2 |^ m) by A2, Lm7;
A7: 1 <= len (Gauge E,m) by GOBRD11:34;
then A8: ((Gauge E,m) * (Center (Gauge E,m)),1) `1 = ((Gauge E,m) * (Center (Gauge E,m)),(len (Gauge E,m))) `1 by A1, Th57;
A9: ( 1 <= Center (Gauge E,m) & Center (Gauge E,m) <= len (Gauge E,m) ) by Lm3;
len (Gauge E,m) = width (Gauge E,m) by JORDAN8:def 1;
then ((Gauge E,m) * (Center (Gauge E,m)),1) `2 <= ((Gauge E,m) * (Center (Gauge E,m)),(len (Gauge E,m))) `2 by A7, A9, SPRECT_3:24;
then A10: (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 A8, GOBOARD7:8;
A11: len (Gauge E,n) = width (Gauge E,n) by JORDAN8:def 1;
then A12: ( ((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, A7, Th57;
[(Center (Gauge E,m)),1] in Indices (Gauge E,m) by A7, Lm4;
then A13: ((Gauge E,m) * (Center (Gauge E,m)),1) `2 = (S-bound E) - (((N-bound E) - (S-bound E)) / (2 |^ m)) by Lm11;
A14: [(Center (Gauge E,n)),j] in Indices (Gauge E,n) by A3, A4, A11, Lm4;
then A15: ((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:56 ;
((N-bound E) - (S-bound E)) / (2 |^ m) >= 0 by A5;
then A16: (S-bound E) - (((N-bound E) - (S-bound E)) / (2 |^ m)) <= (S-bound E) - 0 by XREAL_1:15;
A17: ((N-bound E) - (S-bound E)) / (2 |^ n) >= 0 by A5;

A18: now

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 A14, Lm11;
hence ((Gauge E,m) * (Center (Gauge E,m)),1) `2 <= ((Gauge E,n) * (Center (Gauge E,n)),j) `2 by A6, A13, XREAL_1:15; :: 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:11;
then (((N-bound E) - (S-bound E)) / (2 |^ n)) * (j - 2) >= 0 by A17;
then (S-bound E) + 0 <= (S-bound E) + ((((N-bound E) - (S-bound E)) / (2 |^ n)) * (j - 2)) by XREAL_1:8;
hence ((Gauge E,m) * (Center (Gauge E,m)),1) `2 <= ((Gauge E,n) * (Center (Gauge E,n)),j) `2 by A13, A15, A16, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A19: len (Gauge E,n) = width (Gauge E,n) by JORDAN8:def 1;
A20: ( 1 <= Center (Gauge E,n) & Center (Gauge E,n) <= len (Gauge E,n) ) by Lm3;
then A21: ((Gauge E,n) * (Center (Gauge E,n)),j) `2 <= ((Gauge E,n) * (Center (Gauge E,n)),(len (Gauge E,n))) `2 by A3, A4, A19, SPRECT_3:24;
((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, A9, A20, Th61;
then ((Gauge E,n) * (Center (Gauge E,n)),j) `2 <= ((Gauge E,m) * (Center (Gauge E,m)),(len (Gauge E,m))) `2 by A21, XXREAL_0:2;
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 A12, A18, GOBOARD7:8;
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 A10, TOPREAL1:12; :: thesis: verum