let a, b, g1, M be Real; :: thesis: ( a < b & 0 < g1 & 0 < M implies ex r being Real st

( a < r & r < b & (r - a) * M < g1 ) )

assume that

A1: a < b and

A2: ( 0 < g1 & 0 < M ) ; :: thesis: ex r being Real st

( a < r & r < b & (r - a) * M < g1 )

- b < - a by A1, XREAL_1:24;

then consider r1 being Real such that

A3: ( - b < r1 & r1 < - a ) and

A4: ((- a) - r1) * M < g1 by A2, Th1;

reconsider r = - r1 as Real ;

take r ; :: thesis: ( a < r & r < b & (r - a) * M < g1 )

( - (- b) > - r1 & - r1 > - (- a) ) by A3, XREAL_1:24;

hence ( a < r & r < b & (r - a) * M < g1 ) by A4; :: thesis: verum

( a < r & r < b & (r - a) * M < g1 ) )

assume that

A1: a < b and

A2: ( 0 < g1 & 0 < M ) ; :: thesis: ex r being Real st

( a < r & r < b & (r - a) * M < g1 )

- b < - a by A1, XREAL_1:24;

then consider r1 being Real such that

A3: ( - b < r1 & r1 < - a ) and

A4: ((- a) - r1) * M < g1 by A2, Th1;

reconsider r = - r1 as Real ;

take r ; :: thesis: ( a < r & r < b & (r - a) * M < g1 )

( - (- b) > - r1 & - r1 > - (- a) ) by A3, XREAL_1:24;

hence ( a < r & r < b & (r - a) * M < g1 ) by A4; :: thesis: verum