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 & (b - r) * M < g1 ) )
assume A1: ( a < b & 0 < g1 & 0 < M ) ; :: thesis: ex r being Element of REAL st
( a < r & r < b & (b - r) * M < g1 )
A2: b - (g1 / M) < b by XREAL_1:46, XREAL_1:141, A1;
set r3 = max a,(b - (g1 / M));
max a,(b - (g1 / M)) < b by A2, A1, XXREAL_0:16;
then consider q being real number such that
A3: ( max a,(b - (g1 / M)) < q & q < b ) by XREAL_1:7;
reconsider r = q as Real by XREAL_0:def 1;
take r ; :: thesis: ( a < r & r < b & (b - r) * M < g1 )
A4: a <= max a,(b - (g1 / M)) by XXREAL_0:25;
b - (g1 / M) <= max a,(b - (g1 / M)) by XXREAL_0:25;
then b - (g1 / M) < r by A3, XXREAL_0:2;
then (b - (g1 / M)) - (r - (g1 / M)) < r - (r - (g1 / M)) by XREAL_1:16;
then A5: (b - r) * 1 < g1 / M ;
(b - r) * M < g1 / 1 by A5, A1, XREAL_1:113;
hence ( a < r & r < b & (b - r) * M < g1 ) by A3, A4, XXREAL_0:2; :: thesis: verum