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