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