let a, b be Element of [.0,1.]; min ((a + b),1) in [.0,1.]
A1:
min ((a + b),1) <= 1
by XXREAL_0:17;
A2:
( a >= 0 & b >= 0 )
by XXREAL_1:1;
( min (1,(a + b)) = 1 or min (1,(a + b)) = a + b )
by XXREAL_0:15;
hence
min ((a + b),1) in [.0,1.]
by A1, XXREAL_1:1, A2; verum