let n be Nat; :: thesis: for E being compact non horizontal non vertical Subset of (TOP-REAL 2)

for m, j being Nat st 1 <= m & m <= n & 1 <= j & j <= width (Gauge (E,n)) holds

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)))

let E be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for m, j being Nat st 1 <= m & m <= n & 1 <= j & j <= width (Gauge (E,n)) holds

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)))

let m, j be Nat; :: thesis: ( 1 <= m & m <= n & 1 <= j & j <= width (Gauge (E,n)) implies 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))) )

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,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)))

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 ;

(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, A7;

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 A23, TOPREAL1:6; :: thesis: verum

for m, j being Nat st 1 <= m & m <= n & 1 <= j & j <= width (Gauge (E,n)) holds

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)))

let E be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for m, j being Nat st 1 <= m & m <= n & 1 <= j & j <= width (Gauge (E,n)) holds

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)))

let m, j be Nat; :: thesis: ( 1 <= m & m <= n & 1 <= j & j <= width (Gauge (E,n)) implies 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))) )

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,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)))

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 ;

A7: now :: thesis: for t being Nat st width (Gauge (E,n)) >= t & t >= j holds

(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)))

then A23:
(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)))
by A4;(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)))

let t be Nat; :: thesis: ( width (Gauge (E,n)) >= t & t >= j implies (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))) )

assume that

A8: width (Gauge (E,n)) >= t and

A9: t >= j ; :: thesis: (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)))

A10: len (Gauge (E,m)) = width (Gauge (E,m)) by JORDAN8:def 1;

A11: len (Gauge (E,n)) = width (Gauge (E,n)) by JORDAN8:def 1;

A12: 0 < (N-bound E) - (S-bound E) by SPRECT_1:32, XREAL_1:50;

A13: t >= 1 by A3, A9, XXREAL_0:2;

A14: 0 < 2 |^ m by NEWTON:83;

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 by A1, A2, A8, A10, A11, A13, JORDAN1A:36;

A17: ((Gauge (E,n)) * ((Center (Gauge (E,n))),t)) `1 = ((Gauge (E,n)) * ((Center (Gauge (E,n))),j)) `1 by A1, A2, A3, A4, A8, A11, A13, JORDAN1A:36;

[(Center (Gauge (E,n))),t] in Indices (Gauge (E,n)) by A8, A13, Lm1;

then A18: ((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:52 ;

[(Center (Gauge (E,m))),(width (Gauge (E,m)))] in Indices (Gauge (E,m)) by A10, A15, Lm1;

then A19: ((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;

A20: ((2 |^ m) + 1) / (2 |^ m) >= ((2 |^ n) + 1) / (2 |^ n) by A2, A14, Th1, PREPOWER:93;

t - 2 <= ((2 |^ n) + 3) - 2 by A6, A8, XREAL_1:9;

then (t - 2) / (2 |^ n) <= ((2 |^ n) + 1) / (2 |^ n) by XREAL_1:72;

then (t - 2) / (2 |^ n) <= ((width (Gauge (E,m))) - 2) / (2 |^ m) by A5, A20, 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 A12, XREAL_1:64;

then A21: (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:6;

A22: 1 <= Center (Gauge (E,n)) by JORDAN1B:11;

Center (Gauge (E,n)) <= len (Gauge (E,n)) by JORDAN1B:13;

then ((Gauge (E,n)) * ((Center (Gauge (E,n))),t)) `2 >= ((Gauge (E,n)) * ((Center (Gauge (E,n))),j)) `2 by A3, A8, A9, A22, SPRECT_3:12;

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, A19, A21, GOBOARD7:7; :: thesis: verum

end;assume that

A8: width (Gauge (E,n)) >= t and

A9: t >= j ; :: thesis: (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)))

A10: len (Gauge (E,m)) = width (Gauge (E,m)) by JORDAN8:def 1;

A11: len (Gauge (E,n)) = width (Gauge (E,n)) by JORDAN8:def 1;

A12: 0 < (N-bound E) - (S-bound E) by SPRECT_1:32, XREAL_1:50;

A13: t >= 1 by A3, A9, XXREAL_0:2;

A14: 0 < 2 |^ m by NEWTON:83;

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 by A1, A2, A8, A10, A11, A13, JORDAN1A:36;

A17: ((Gauge (E,n)) * ((Center (Gauge (E,n))),t)) `1 = ((Gauge (E,n)) * ((Center (Gauge (E,n))),j)) `1 by A1, A2, A3, A4, A8, A11, A13, JORDAN1A:36;

[(Center (Gauge (E,n))),t] in Indices (Gauge (E,n)) by A8, A13, Lm1;

then A18: ((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:52 ;

[(Center (Gauge (E,m))),(width (Gauge (E,m)))] in Indices (Gauge (E,m)) by A10, A15, Lm1;

then A19: ((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;

A20: ((2 |^ m) + 1) / (2 |^ m) >= ((2 |^ n) + 1) / (2 |^ n) by A2, A14, Th1, PREPOWER:93;

t - 2 <= ((2 |^ n) + 3) - 2 by A6, A8, XREAL_1:9;

then (t - 2) / (2 |^ n) <= ((2 |^ n) + 1) / (2 |^ n) by XREAL_1:72;

then (t - 2) / (2 |^ n) <= ((width (Gauge (E,m))) - 2) / (2 |^ m) by A5, A20, 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 A12, XREAL_1:64;

then A21: (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:6;

A22: 1 <= Center (Gauge (E,n)) by JORDAN1B:11;

Center (Gauge (E,n)) <= len (Gauge (E,n)) by JORDAN1B:13;

then ((Gauge (E,n)) * ((Center (Gauge (E,n))),t)) `2 >= ((Gauge (E,n)) * ((Center (Gauge (E,n))),j)) `2 by A3, A8, A9, A22, SPRECT_3:12;

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, A19, A21, GOBOARD7:7; :: thesis: verum

(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, A7;

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 A23, TOPREAL1:6; :: thesis: verum