theorem Th1: :: INTEGR10:1
for a, b, g1, M being Real st a < b & 0 < g1 & 0 < M holds
ex r being Real st
( a < r & r < b & (b - r) * M < g1 )