let m, j, i, n be Nat; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds
ex i1, j1 being Nat st
( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) & 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) implies ex i1, j1 being Nat st
( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) & 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) ) )
assume that
A1: m <= n and
A2: ( 1 <= i & i + 1 <= len (Gauge (C,n)) ) and
A3: ( 1 <= j & j + 1 <= width (Gauge (C,n)) ) ; :: thesis: ex i1, j1 being Nat st
( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) & 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )
consider i1, j1 being Nat such that
A4: i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] and
A5: j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] and
A6: cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) by A1, A2, A3, Th37;
take i1 ; :: thesis: ex j1 being Nat st
( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) & 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )
take j1 ; :: thesis: ( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) & 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )
thus ( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) ) by A1, A2, A4, Th36; :: thesis: ( 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )
( len (Gauge (C,m)) = width (Gauge (C,m)) & len (Gauge (C,n)) = width (Gauge (C,n)) ) by JORDAN8:def 1;
hence ( 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) ) by A1, A3, A5, Th36; :: thesis: cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1)
thus cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) by A6; :: thesis: verum