theorem
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 )