:: deftheorem II3Def defines I_I3 FUZIMPL4:def 4 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = I_I3 iff for x, y being Element of [.0,1.] holds
( ( ( x = 0 or y <> 0 ) implies b₁ . (x,y) = 1 ) & ( x <> 0 & y = 0 implies b₁ . (x,y) = 0 ) ) );