let a, b be Element of [.0,1.]; :: thesis: (a * b) / ((a + b) - (a * b)) in [.0,1.]
A1: a * b in [.0,1.] by Lemma1;
(a + b) - (a * b) in [.0,1.] by abMinab01;
then A2: (a + b) - (a * b) >= 0 by XXREAL_1:1;
T0: a * b >= 0 by A1, XXREAL_1:1;
( 0 <= a & b <= 1 ) by XXREAL_1:1;
then S1: a * b <= a by XREAL_1:153;
( 0 <= b & a <= 1 ) by XXREAL_1:1;
then a * b <= b by XREAL_1:153;
then (a * b) + (a * b) <= a + b by S1, XREAL_1:7;
then a * b <= (a + b) - (a * b) by XREAL_1:19;
then (a * b) / ((a + b) - (a * b)) <= 1 by XREAL_1:183, T0;
hence (a * b) / ((a + b) - (a * b)) in [.0,1.] by T0, A2, XXREAL_1:1; :: thesis: verum