:: deftheorem Def4 defines categorial CAT_5:def 4 :
for IT being set holds
( IT is categorial iff for x being set st x in IT holds
x is Category );