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