:: deftheorem defines " QUATERN2:def 2 :
for c being quaternion number holds c " = 1q / c;