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

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

assume that

A1: a < b and

A2: 0 < g1 and

A3: 0 < M ; :: thesis: ex r being Real st

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

set r3 = max (a,(b - (g1 / M)));

b - (g1 / M) < b by A2, A3, XREAL_1:44, XREAL_1:139;

then max (a,(b - (g1 / M))) < b by A1, XXREAL_0:16;

then consider q being Real such that

A4: max (a,(b - (g1 / M))) < q and

A5: q < b by XREAL_1:5;

reconsider r = q as Real ;

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

b - (g1 / M) <= max (a,(b - (g1 / M))) by XXREAL_0:25;

then b - (g1 / M) < r by A4, XXREAL_0:2;

then (b - (g1 / M)) - (r - (g1 / M)) < r - (r - (g1 / M)) by XREAL_1:14;

then (b - r) * 1 < g1 / M ;

then ( a <= max (a,(b - (g1 / M))) & (b - r) * M < g1 / 1 ) by A3, XREAL_1:111, XXREAL_0:25;

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

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

assume that

A1: a < b and

A2: 0 < g1 and

A3: 0 < M ; :: thesis: ex r being Real st

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

set r3 = max (a,(b - (g1 / M)));

b - (g1 / M) < b by A2, A3, XREAL_1:44, XREAL_1:139;

then max (a,(b - (g1 / M))) < b by A1, XXREAL_0:16;

then consider q being Real such that

A4: max (a,(b - (g1 / M))) < q and

A5: q < b by XREAL_1:5;

reconsider r = q as Real ;

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

b - (g1 / M) <= max (a,(b - (g1 / M))) by XXREAL_0:25;

then b - (g1 / M) < r by A4, XXREAL_0:2;

then (b - (g1 / M)) - (r - (g1 / M)) < r - (r - (g1 / M)) by XREAL_1:14;

then (b - r) * 1 < g1 / M ;

then ( a <= max (a,(b - (g1 / M))) & (b - r) * M < g1 / 1 ) by A3, XREAL_1:111, XXREAL_0:25;

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