theorem :: CAT_4:34

for C being Cartesian_category
for a being Object of C holds Hom (a,(a [x] a)) <> {}