:: deftheorem I2Def defines I_{-2} FUZIMPL1:def 10 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = I_{-2} iff for x, y being Element of [.0,1.] holds b₁ . (x,y) = max (y,(min ((1 - x),(1 - y)))) );