let UN be non trivial Universe; :: thesis: QUATERNION in UN
A1: QUATERNION c= (Funcs (4,REAL)) \/ COMPLEX by XBOOLE_1:13;
( 4 in UN & REAL is Element of UN ) by Th16, Th53;
then ( Funcs (4,REAL) in UN & COMPLEX in UN ) by Th55, CLASSES2:61;
then (Funcs (4,REAL)) \/ COMPLEX in UN by CLASSES2:60;
hence QUATERNION in UN by A1, Th13; :: thesis: verum