theorem Th48: :: NUMBER17:48

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