let a, b be Element of [.0,1.]; ((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; verum