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