for a, b being Element of [.0,1.] holds max (a,b) in [.0,1.]