theorem Th19: :: CAT_4:19

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