let A, B, C, D be category; :: thesis: ( A,B are_opposite & C,D are_opposite & A,C are_isomorphic implies B,D are_isomorphic )
assume A1: ( A,B are_opposite & C,D are_opposite ) ; :: thesis: ( not A,C are_isomorphic or B,D are_isomorphic )
then ( A,C are_isomorphic implies B,C are_anti-isomorphic ) by Th18;
hence ( not A,C are_isomorphic or B,D are_isomorphic ) by A1, Th18; :: thesis: verum