theorem :: CAT_1:13

for o, m being set
for a, b being Object of (1Cat (o,m)) holds Hom (a,b) <> {} by Th9;