:: deftheorem defines Ob CAT_6:def 17 :
for C being CategoryStr holds Ob C = { f where f is morphism of C : ( f is identity & f in Mor C ) } ;