let n be Element of NAT ; :: thesis:
let E be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis:
let m, j be Element of NAT ; :: thesis:
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:
A5: width (Gauge E,m) = len (Gauge E,m) by JORDAN8:def 1
.= (2 |^ m) + 3 by JORDAN8:def 1 ;
A6: width (Gauge E,n) = len (Gauge E,n) by JORDAN8:def 1
.= (2 |^ n) + 3 by JORDAN8:def 1 ;

now

let t be Element of NAT ; :: thesis:
assume that
A7: width (Gauge E,n) >= t and
A8: t >= j ; :: thesis:
A9: len (Gauge E,m) = width (Gauge E,m) by JORDAN8:def 1;
A10: len (Gauge E,n) = width (Gauge E,n) by JORDAN8:def 1;
A11: 0 < (N-bound E) - (S-bound E) by SPRECT_1:34, XREAL_1:52;
A12: t >= 1 by A3, A8, XXREAL_0:2;
A13: 0 < 2 |^ m by NEWTON:102;
A15: 1 <= len (Gauge E,m) by GOBRD11:34;
then A16: ( ((Gauge E,m) * (Center (Gauge E,m)),(width (Gauge E,m))) `1 = ((Gauge E,n) * (Center (Gauge E,n)),t) `1 & ((Gauge E,n) * (Center (Gauge E,n)),t) `1 = ((Gauge E,n) * (Center (Gauge E,n)),j) `1 ) by A1, A2, A3, A4, A7, A9, A10, A12, JORDAN1A:57;
[(Center (Gauge E,n)),t] in Indices (Gauge E,n) by A7, A12, Lm1;
then A17: ((Gauge E,n) * (Center (Gauge E,n)),t) `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)) * (t - 2)))]| `2 by JORDAN8:def 1
.= (S-bound E) + ((((N-bound E) - (S-bound E)) / (2 |^ n)) * (t - 2)) by EUCLID:56 ;
[(Center (Gauge E,m)),(width (Gauge E,m))] in Indices (Gauge E,m) by A9, A15, Lm1;
then A18: ((Gauge E,m) * (Center (Gauge E,m)),(width (Gauge E,m))) `2 = (S-bound E) + ((((N-bound E) - (S-bound E)) / (2 |^ m)) * ((width (Gauge E,m)) - 2)) by Lm2;
A19: ((2 |^ m) + 1) / (2 |^ m) >= ((2 |^ n) + 1) / (2 |^ n) by A2, A13, Th1, PREPOWER:107;
t - 2 <= ((2 |^ n) + 3) - 2 by A6, A7, XREAL_1:11;
then (t - 2) / (2 |^ n) <= ((2 |^ n) + 1) / (2 |^ n) by XREAL_1:74;
then (t - 2) / (2 |^ n) <= ((width (Gauge E,m)) - 2) / (2 |^ m) by A5, A19, XXREAL_0:2;
then ((N-bound E) - (S-bound E)) * ((t - 2) / (2 |^ n)) <= ((N-bound E) - (S-bound E)) * (((width (Gauge E,m)) - 2) / (2 |^ m)) by A11, XREAL_1:66;
then (((N-bound E) - (S-bound E)) / (2 |^ n)) * (t - 2) <= ((N-bound E) - (S-bound E)) * (((width (Gauge E,m)) - 2) / (2 |^ m)) ;
then (((N-bound E) - (S-bound E)) / (2 |^ m)) * ((width (Gauge E,m)) - 2) >= (((N-bound E) - (S-bound E)) / (2 |^ n)) * (t - 2) ;
then A20: (S-bound E) + ((((N-bound E) - (S-bound E)) / (2 |^ m)) * ((width (Gauge E,m)) - 2)) >= (S-bound E) + ((((N-bound E) - (S-bound E)) / (2 |^ n)) * (t - 2)) by XREAL_1:8;
( 1 <= Center (Gauge E,n) & Center (Gauge E,n) <= len (Gauge E,n) ) by JORDAN1B:12, JORDAN1B:14;
then ((Gauge E,n) * (Center (Gauge E,n)),t) `2 >= ((Gauge E,n) * (Center (Gauge E,n)),j) `2 by A3, A7, A8, SPRECT_3:24;
hence (Gauge E,n) * (Center (Gauge E,n)),t in LSeg ((Gauge E,m) * (Center (Gauge E,m)),(width (Gauge E,m))),((Gauge E,n) * (Center (Gauge E,n)),j) by A16, A17, A18, A20, GOBOARD7:8; :: thesis:

end;

then ( (Gauge E,n) * (Center (Gauge E,n)),(width (Gauge E,n)) in LSeg ((Gauge E,m) * (Center (Gauge E,m)),(width (Gauge E,m))),((Gauge E,n) * (Center (Gauge E,n)),j) & (Gauge E,n) * (Center (Gauge E,n)),j in LSeg ((Gauge E,m) * (Center (Gauge E,m)),(width (Gauge E,m))),((Gauge E,n) * (Center (Gauge E,n)),j) ) by A4;
hence LSeg ((Gauge E,n) * (Center (Gauge E,n)),(width (Gauge E,n))),((Gauge E,n) * (Center (Gauge E,n)),j) c= LSeg ((Gauge E,m) * (Center (Gauge E,m)),(width (Gauge E,m))),((Gauge E,n) * (Center (Gauge E,n)),j) by TOPREAL1:12; :: thesis: