:: deftheorem Def17 defines compl3 MOD_2:def 17 :
for b₁ being UnOp of {0,1,2} holds
( b₁ = compl3 iff for a being Element of {0,1,2} holds b₁ . a = - a );