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