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