theorem Th29:
for
C being non
empty compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n,
i1,
i2 being
Nat st 1
<= i1 &
i1 + 1
<= len (Gauge (C,n)) &
N-min C in cell (
(Gauge (C,n)),
i1,
((width (Gauge (C,n))) -' 1)) &
N-min C <> (Gauge (C,n)) * (
i1,
((width (Gauge (C,n))) -' 1)) & 1
<= i2 &
i2 + 1
<= len (Gauge (C,n)) &
N-min C in cell (
(Gauge (C,n)),
i2,
((width (Gauge (C,n))) -' 1)) &
N-min C <> (Gauge (C,n)) * (
i2,
((width (Gauge (C,n))) -' 1)) holds
i1 = i2