theorem Th24: :: CAT_4:24

for C being Cartesian_category
for a, b being Object of C holds <:(pr1 (a,b)),(pr2 (a,b)):> = id (a [x] b)