:: deftheorem defines - QUATERNI:def 8 :
for x, y being quaternion number holds x - y = x + (- y);