theorem Th30: :: JORDAN9:30

for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat
for f being non constant standard special_circular_sequence st f is_sequence_on Gauge (C,n) & ( for k being Nat st 1 <= k & k + 1 <= len f holds
( left_cell (f,k,(Gauge (C,n))) misses C & right_cell (f,k,(Gauge (C,n))) meets C ) ) & ex i being Nat st
( 1 <= i & i + 1 <= len (Gauge (C,n)) & f /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) & f /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))) & N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) & N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) ) holds
N-min (L~ f) = f /. 1