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