:: deftheorem Def7 defines cat CAT_5:def 7 :
for a being object st a is Category holds
cat a = a;