let C be Cartesian_category; :: thesis: for a being Object of C holds term a = term (a,([1] C))
let a be Object of C; :: thesis: term a = term (a,([1] C))
[1] C is terminal by Def8;
hence term a = term (a,([1] C)) by CAT_3:37; :: thesis: verum