:: deftheorem DefDecr defines decreasing_on_1st FUZIMPL1:def 1 :
for f being BinOp of [.0,1.] holds
( f is decreasing_on_1st iff for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds
f . (x1,y) >= f . (x2,y) );