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