:: deftheorem DefIncr defines increasing_on_2nd FUZIMPL1:def 2 :
for f being BinOp of [.0,1.] holds
( f is increasing_on_2nd iff for x, y1, y2 being Element of [.0,1.] st y1 <= y2 holds
f . (x,y1) <= f . (x,y2) );