:: deftheorem defines Mor CAT_6:def 1 :
for C being CategoryStr holds Mor C = the carrier of C;