:: deftheorem defines Alter ALTCAT_2:def 5 :
for C being Category holds Alter C = AltCatStr(# the carrier of C,(the_hom_sets_of C),(the_comps_of C) #);