:: deftheorem I5Def defines I_{-5} FUZIMPL1:def 13 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = I_{-5} iff for x, y being Element of [.0,1.] holds b₁ . (x,y) = 1 );