theorem Th31: :: CAT_4:31

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