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