theorem Th31: :: BKMODEL4:3

for a, b, c being Real st 0 <= a & a <= 1 & 0 < b * c holds
( 0 <= (a * c) / (((1 - a) * b) + (a * c)) & (a * c) / (((1 - a) * b) + (a * c)) <= 1 )