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

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