:: deftheorem Def22 defines GroupObjects GRCAT_1:def 24 :
for UN being Universe
for b₂ being set holds
( b₂ = GroupObjects UN iff for y being object holds
( y in b₂ iff ex x being object st
( x in UN & GO x,y ) ) );