let a, b be Element of [.0,1.]; (a + b) - (a * b) in [.0,1.]
S1:
1 - b in [.0,1.]
by OpIn01;
then
a * (1 - b) in [.0,1.]
by Lemma1;
then B1:
a * (1 - b) >= 0
by XXREAL_1:1;
a0:
b >= 0
by XXREAL_1:1;
S2:
( a <= 1 & b <= 1 )
by XXREAL_1:1;
( 0 <= 1 - b & 1 - b <= 1 )
by S1, XXREAL_1:1;
then
a * (1 - b) <= 1 * (1 - b)
by S2, XREAL_1:64;
then
(a * (1 - b)) + b <= (1 - b) + b
by XREAL_1:6;
hence
(a + b) - (a * b) in [.0,1.]
by XXREAL_1:1, a0, B1; verum