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

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