let m, j, i, n be Nat; 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); ( 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)) )
; 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
; 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
; ( 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; ( 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; 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; verum