:: deftheorem defines opp OPPCAT_1:def 1 :
for C being Category holds C opp = CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #);