theorem Th28: :: CAT_4:28

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