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