let C be Category; :: thesis: for x being set holds
( x is coIndexing of C iff x is Indexing of (C opp ) )
let x be set ; :: thesis: ( x is coIndexing of C iff x is Indexing of (C opp ) )
C opp = CatStr(# the carrier of C,the carrier' of C,the Target of C,the Source of C,(~ the Comp of C),the Id of C #) by OPPCAT_1:def 1;
hence ( x is coIndexing of C iff x is Indexing of (C opp ) ) ; :: thesis: verum