let a, b be Real; :: thesis: ( 0 < a implies ex m being Nat st 0 < (a * m) + b )
assume A1: 0 < a ; :: thesis: ex m being Nat st 0 < (a * m) + b
then A2: ((- b) / a) * a = - b by XCMPLX_1:87;
consider m being Nat such that
A3: - (b / a) < m by SEQ_4:3;
take m ; :: thesis: 0 < (a * m) + b
(- (b / a)) * a < m * a by A1, A3, XREAL_1:68;
then (- b) + b < (a * m) + b by A2, XREAL_1:8;
hence 0 < (a * m) + b ; :: thesis: verum