:: deftheorem defines Hom ENS_1:def 18 :
for C being Category holds Hom C = { (Hom (a,b)) where a, b is Object of C : verum } ;