for C being Category
for a, b being Element of C st Hom (a,b) <> {} holds
ex m being Morphism of a,b st m in Hom (a,b)