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