let C be Cartesian_category; :: thesis: for a, b being Object of C holds Hom ((a [x] b),(b [x] a)) <> {}
let a, b be Object of C; :: thesis: Hom ((a [x] b),(b [x] a)) <> {}
( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} ) by Th19;
hence Hom ((a [x] b),(b [x] a)) <> {} by Th23; :: thesis: verum