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