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

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