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) )
A1: IdMap C = IdMap (C opp) by Lm2;
thus ( x is coIndexing of C iff x is Indexing of (C opp) ) by A1; :: thesis: verum