for C being Simple_closed_curve
for p being Point of (TOP-REAL 2) st p in BDD C holds
ex n, i, j being Nat st
( 1 < i & i < len (Gauge (C,n)) & 1 < j & j < width (Gauge (C,n)) & p `1 <> ((Gauge (C,n)) * (i,j)) `1 & p in cell ((Gauge (C,n)),i,j) & cell ((Gauge (C,n)),i,j) c= BDD C )