:: deftheorem Def1 defines Gauge JORDAN8:def 1 :
for C being Subset of (TOP-REAL 2)
for n being natural Number
for b3 being Matrix of (TOP-REAL 2) holds
( b3 = Gauge (C,n) iff ( len b3 = (2 |^ n) + 3 & len b3 = width b3 & ( for i, j being Nat st [i,j] in Indices b3 holds
b3 * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) ) );