:: deftheorem LukNorm defines Lukasiewicz_norm FUZNORM1:def 10 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = Lukasiewicz_norm iff for a, b being Element of [.0,1.] holds b₁ . (a,b) = max (0,((a + b) - 1)) );