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