let m, n, i, j be Element of 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 Element of 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 Element of 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 Element of 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 Element of 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, Th43;
take i1 ; :: thesis: ex j1 being Element of 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, Th42; :: 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, Th42; :: 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