let C be Cartesian_category; :: thesis: for a being Object of C holds Hom (a,(a [x] a)) <> {}
let a be Object of C; :: thesis: Hom (a,(a [x] a)) <> {}
Hom (a,a) <> {} by CAT_1:27;
hence Hom (a,(a [x] a)) <> {} by Th25; :: thesis: verum