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