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