take <k> ; :: thesis: <k> is quaternion
thus <k> is quaternion ; :: thesis: verum