:: deftheorem defines TolCat COH_SP:def 29 :
for X being set holds TolCat X = CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X) #);