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 Def9;
hence Hom a,([1] C) <> {} by CAT_1:def 15; :: thesis: verum