:: deftheorem defines cod GRCAT_1:def 3 :
for C being Category
for O being non empty Subset of the carrier of C holds cod O = the Target of C | (Morphs O);