let m, n be Element of NAT ; for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= m & m <= n holds
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)))
let E be compact non horizontal non vertical Subset of (TOP-REAL 2); ( 1 <= m & m <= n implies 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))) )
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
; ( not m <= n or 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))) )
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
; 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)))
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:34, XREAL_1:52;
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:24;
[(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:9;
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:15;
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:8;
( ((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:8;
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:12; verum