:: deftheorem Def7 defines reflexive CAT_1:def 9 :
for C being non empty non void CatStr holds
( C is reflexive iff for b being Element of C holds Hom (b,b) <> {} );