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