let a, b be Element of [.0,1.]; :: thesis: min (1,((1 - a) + b)) in [.0,1.]
A1: min (1,((1 - a) + b)) <= 1 by XXREAL_0:17;
1 - a in [.0,1.] by FUZNORM1:7;
then ( 1 - a >= 0 & b >= 0 ) by XXREAL_1:1;
then min (1,((1 - a) + b)) >= 0 by XXREAL_0:20;
hence min (1,((1 - a) + b)) in [.0,1.] by A1, XXREAL_1:1; :: thesis: verum