:: deftheorem Def11 defines min_at FINSEQ_6:def 8 :
for F being FinSequence of INT
for m, n being Nat st 1 <= m & m <= n & n <= len F holds
for b₄ being Nat holds
( b₄ = min_at (F,m,n) iff ex X being non empty finite Subset of INT st
( X = rng ((m,n) -cut F) & b₄ + 1 = ((min X) .. ((m,n) -cut F)) + m ) );