:: deftheorem Def7 defines - QUATERNI:def 7 :
for z, b₂ being Quaternion holds
( b₂ = - z iff z + b₂ = 0 );