let a, b be Element of [.0,1.]; :: thesis: ((a + b) - ((2 * a) * b)) / (1 - (a * b)) in [.0,1.]

( 0 <= a & b <= 1 ) by XXREAL_1:1;

then S1: a * b <= a by XREAL_1:153;

S2: ( 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 S5: (a * b) - (a * b) <= ((a + b) - (a * b)) - (a * b) by XREAL_1:9, XREAL_1:19;

1 - b in [.0,1.] by OpIn01;

then 1 - b >= 0 by XXREAL_1:1;

then a * (1 - b) <= 1 * (1 - b) by S2, XREAL_1:64;

then (a - (a * b)) + b <= (1 - b) + b by XREAL_1:6;

then ((a + b) - (a * b)) - (a * b) <= 1 - (a * b) by XREAL_1:9;

then B9: ((a + b) - ((2 * a) * b)) / (1 - (a * b)) <= 1 by XREAL_1:183, S5;

a * b in [.0,1.] by Lemma1;

then a * b <= 1 by XXREAL_1:1;

then 1 - (a * b) >= 1 - 1 by XREAL_1:10;

hence ((a + b) - ((2 * a) * b)) / (1 - (a * b)) in [.0,1.] by XXREAL_1:1, B9, S5; :: thesis: verum

( 0 <= a & b <= 1 ) by XXREAL_1:1;

then S1: a * b <= a by XREAL_1:153;

S2: ( 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 S5: (a * b) - (a * b) <= ((a + b) - (a * b)) - (a * b) by XREAL_1:9, XREAL_1:19;

1 - b in [.0,1.] by OpIn01;

then 1 - b >= 0 by XXREAL_1:1;

then a * (1 - b) <= 1 * (1 - b) by S2, XREAL_1:64;

then (a - (a * b)) + b <= (1 - b) + b by XREAL_1:6;

then ((a + b) - (a * b)) - (a * b) <= 1 - (a * b) by XREAL_1:9;

then B9: ((a + b) - ((2 * a) * b)) / (1 - (a * b)) <= 1 by XREAL_1:183, S5;

a * b in [.0,1.] by Lemma1;

then a * b <= 1 by XXREAL_1:1;

then 1 - (a * b) >= 1 - 1 by XREAL_1:10;

hence ((a + b) - ((2 * a) * b)) / (1 - (a * b)) in [.0,1.] by XXREAL_1:1, B9, S5; :: thesis: verum