theorem Max1In01: :: FUZIMPL1:4

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