:: deftheorem defines cat GRCAT_1:def 6 :
for C being Category
for O being non empty Subset of the carrier of C holds cat O = CatStr(# O,(Morphs O),(dom O),(cod O),(comp O) #);