:: deftheorem I1Def defines I_{-1} FUZIMPL1:def 9 :
for b1 being BinOp of [.0,1.] holds
( b1 = I_{-1} iff for x, y being Element of [.0,1.] holds b1 . (x,y) = max ((1 - x),(min (x,y))) );