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