let a, b, g1, M be real number ; :: thesis: ( a < b & 0 < g1 & 0 < M implies ex r being Element of REAL st
( a < r & r < b & (r - a) * M < g1 ) )
assume A1: ( a < b & 0 < g1 & 0 < M ) ; :: thesis: ex r being Element of REAL st
( a < r & r < b & (r - a) * M < g1 )
A2: - b < - a by A1, XREAL_1:26;
consider r1 being Real such that
A3: ( - b < r1 & r1 < - a & ((- a) - r1) * M < g1 ) by A1, A2, Th1;
reconsider r = - r1 as Real ;
take r ; :: thesis: ( a < r & r < b & (r - a) * M < g1 )
A4: - (- b) > - r1 by A3, XREAL_1:26;
- r1 > - (- a) by A3, XREAL_1:26;
hence ( a < r & r < b & (r - a) * M < g1 ) by A3, A4; :: thesis: verum