let c be Element of R_Quaternion; :: thesis: c is quaternion
c in the carrier of R_Quaternion ;
then c in QUATERNION by Def10;
hence c is quaternion ; :: thesis: verum