:: deftheorem Kleene defines Kleene-Dienes_implication FUZIMPL1:def 18 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = Kleene-Dienes_implication iff for x, y being Element of [.0,1.] holds b₁ . (x,y) = max ((1 - x),y) );