:: deftheorem defines comp GRCAT_1:def 4 :
for C being Category
for O being non empty Subset of the carrier of C holds comp O = the Comp of C || (Morphs O);