:: deftheorem Def2 defines quaternion QUATERNI:def 2 :
for x being Number holds
( x is quaternion iff x in QUATERNION );