:: deftheorem defines satisfying_(LB) FUZIMPL1:def 26 :
for f being BinOp of [.0,1.] holds
( f is satisfying_(LB) iff for y being Element of [.0,1.] holds f . (0,y) = 1 );