for x being Element of RingObjects UN holds x is strict Ring by Th23;
hence RingObjects UN is Ring_DOMAIN-like by Def12; :: thesis: verum