theorem Th1: :: BASEL_1:1

for a, b being Real st 0 < a holds
ex m being Nat st 0 < (a * m) + b