let a, b be Element of [.0,1.]; :: thesis: max (0,((a + b) - 1)) in [.0,1.]
A1: max (0,((a + b) - 1)) >= 0 by XXREAL_0:25;
( a <= 1 & b <= 1 ) by XXREAL_1:1;
then a + b <= 1 + 1 by XREAL_1:7;
then A2: (a + b) - 1 <= 2 - 1 by XREAL_1:9;
( max (0,((a + b) - 1)) = 0 or max (0,((a + b) - 1)) = (a + b) - 1 ) by XXREAL_0:16;
hence max (0,((a + b) - 1)) in [.0,1.] by A1, XXREAL_1:1, A2; :: thesis: verum