theorem :: NUMBER17:46

for f being 2 -element natural-valued increasing positive FinSequence ex a, b being positive Nat st
( f = <*a,b*> & a < b )