:: deftheorem defines op3 LATTBA_1:def 1 :
for b₁ being TriOp of {0} holds
( b₁ = op3 iff b₁ . (0,0,0) = 0 );