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