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