:: deftheorem defines Morphs GRCAT_1:def 1 :
for C being Category
for O being non empty Subset of the carrier of C holds Morphs O = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;