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