:: deftheorem defines alter CAT_6:def 34 :
for A being Category holds alter A = CategoryStr(# the carrier' of A, the Comp of A #);