theorem Th18: :: CAT_4:18

for C being Cartesian_category
for a, b being Object of C holds
( dom (pr2 (a,b)) = a [x] b & cod (pr2 (a,b)) = b )