:: deftheorem MinDef defines minnorm FUZNORM1:def 6 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = minnorm iff for a, b being Element of [.0,1.] holds b₁ . (a,b) = min (a,b) );