theorem :: GOBRD14:8

for i, j being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st i <= j holds
for a, b being Nat st 2 <= a & a <= (len (Gauge (C,i))) - 1 & 2 <= b & b <= (len (Gauge (C,i))) - 1 holds
ex c, d being Nat st
( 2 <= c & c <= (len (Gauge (C,j))) - 1 & 2 <= d & d <= (len (Gauge (C,j))) - 1 & [c,d] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * (c,d) & c = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) )