theorem :: CAT_4:11

for C being Cartesian_category holds [1] C is terminal by Def8;