let UN be Universe; :: thesis: Z_3 in RingObjects UN
ex x being object st
( x in UN & GO x, Z_3 ) by Th16;
hence Z_3 in RingObjects UN by Def16; :: thesis: verum