:: deftheorem defines RingCat RINGCAT1:def 24 :
for UN being Universe holds RingCat UN = CatStr(# (RingObjects UN),(Morphs (RingObjects UN)),(dom (RingObjects UN)),(cod (RingObjects UN)),(comp (RingObjects UN)) #);