:: deftheorem Yager defines Yager_implication FUZIMPL1:def 21 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = Yager_implication iff for x, y being Element of [.0,1.] holds
( ( x = y & y = 0 implies b₁ . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies b₁ . (x,y) = y to_power x ) ) );