:: deftheorem defines opp CAT_6:def 13 :
for C being CategoryStr holds C opp = CategoryStr(# the carrier of C,(~ the composition of C) #);