:: deftheorem Def3 defines opp CAT_3:def 3 :
for C being Category
for I being set
for F being Function of I, the carrier' of C
for b₄ being Function of I, the carrier' of (C opp) holds
( b₄ = F opp iff for x being set st x in I holds
b₄ /. x = (F /. x) opp );