:: deftheorem Def16 defines RingObjects RINGCAT1:def 16 :
for UN being Universe
for b₂ being set holds
( b₂ = RingObjects UN iff for y being object holds
( y in b₂ iff ex x being set st
( x in UN & GO x,y ) ) );