:: deftheorem Luk defines Lukasiewicz_implication FUZIMPL1:def 14 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = Lukasiewicz_implication iff for x, y being Element of [.0,1.] holds b₁ . (x,y) = min (1,((1 - x) + y)) );