let a, b, g1, M be Real; ( 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 )
; 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
; ( 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; verum