let a, b be Element of [.0,1.]; :: thesis: max (b,(min ((1 - a),(1 - b)))) in [.0,1.]
a1: ( 1 - a in [.0,1.] & 1 - b in [.0,1.] ) by FUZNORM1:7;
( max (b,(min ((1 - a),(1 - b)))) = b or max (b,(min ((1 - a),(1 - b)))) = min ((1 - a),(1 - b)) ) by XXREAL_0:16;
hence max (b,(min ((1 - a),(1 - b)))) in [.0,1.] by a1, FUZNORM1:1; :: thesis: verum