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