let a, b, c be Real; :: thesis: ( 0 <= a & a <= 1 & 0 < b * c implies ( 0 <= (a * c) / (((1 - a) * b) + (a * c)) & (a * c) / (((1 - a) * b) + (a * c)) <= 1 ) )
assume that
A1: ( 0 <= a & a <= 1 ) and
A2: 0 < b * c ; :: thesis: ( 0 <= (a * c) / (((1 - a) * b) + (a * c)) & (a * c) / (((1 - a) * b) + (a * c)) <= 1 )

per cases ( ( 0 < b & 0 < c ) or ( b < 0 & c < 0 ) ) by A2, XREAL_1:134;

suppose A3: ( 0 < b & 0 < c ) ; :: thesis: ( 0 <= (a * c) / (((1 - a) * b) + (a * c)) & (a * c) / (((1 - a) * b) + (a * c)) <= 1 )

B3: a - a <= 1 - a by A1, XREAL_1:9;
hence 0 <= (a * c) / (((1 - a) * b) + (a * c)) by A1, A3; :: thesis: (a * c) / (((1 - a) * b) + (a * c)) <= 1
0 + (a * c) <= ((1 - a) * b) + (a * c) by A3, B3, XREAL_1:6;
hence (a * c) / (((1 - a) * b) + (a * c)) <= 1 by A1, A3, XREAL_1:183; :: thesis: verum

end;

suppose A4: ( b < 0 & c < 0 ) ; :: thesis: ( 0 <= (a * c) / (((1 - a) * b) + (a * c)) & (a * c) / (((1 - a) * b) + (a * c)) <= 1 )

A5: a - a <= 1 - a by A1, XREAL_1:9;
hence 0 <= (a * c) / (((1 - a) * b) + (a * c)) by A1, A4; :: thesis: (a * c) / (((1 - a) * b) + (a * c)) <= 1
((1 - a) * b) + (a * c) <= 0 + (a * c) by A4, A5, XREAL_1:6;
hence (a * c) / (((1 - a) * b) + (a * c)) <= 1 by A1, A4, XREAL_1:184; :: thesis: verum

end;

end;