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