let UN be Universe; :: thesis: Z3 in RingObjects UN
ex x being set st
( x in UN & GO x, Z3 ) by Th21;
hence Z3 in RingObjects UN by Def17; :: thesis: verum