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