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:56;
hence Hom a,(a [x] a) <> {} by Th25; :: thesis: verum