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