:: deftheorem defines <= FUZNORM1:def 16 :
for f1, f2 being BinOp of [.0,1.] holds
( f1 <= f2 iff for a, b being Element of [.0,1.] holds f1 . (a,b) <= f2 . (a,b) );