let C be Cartesian_category; :: thesis: for a being Object of C holds Hom (a,([1] C)) <> {}
let a be Object of C; :: thesis: Hom (a,([1] C)) <> {}
[1] C is terminal by Def8;
hence Hom (a,([1] C)) <> {} ; :: thesis: verum