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