:: deftheorem I4Def defines I_{-4} FUZIMPL1:def 12 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = I_{-4} iff for x, y being Element of [.0,1.] holds
( ( x = 0 implies b₁ . (x,y) = 1 ) & ( x > 0 implies b₁ . (x,y) = 0 ) ) );