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