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

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; :: thesis: verum