theorem :: JORDAN1J:42

for n being Nat
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i + 1 <= len (Gauge (C,n)) & W-min C in cell ((Gauge (C,n)),1,i) & W-min C <> (Gauge (C,n)) * (2,i) )