for UN being Universe
for a being Object of (GroupCat UN)
for aa being Element of GroupObjects UN st a = aa holds
id a = ID aa