:: deftheorem defines compquaternion QUATERN2:def 3 :
for b₁ being UnOp of QUATERNION holds
( b₁ = compquaternion iff for c being Element of QUATERNION holds b₁ . c = - c );