theorem Th115: :: NUMBER17:115

for s being positive Nat
for f being b₁ -element natural-valued increasing positive-yielding FinSequence holds Sierp162FS_2 f is increasing