:: deftheorem defines satisfying_(OP) FUZIMPL2:def 4 :
for I being BinOp of [.0,1.] holds
( I is satisfying_(OP) iff for x, y being Element of [.0,1.] holds
( I . (x,y) = 1 iff x <= y ) );