theorem :: INDEX_1:8

for C being Category
for x being set holds
( x is coIndexing of C iff x is Indexing of (C opp) ) by Lm2;