:: deftheorem defines categorial CAT_5:def 5 :
for X being non empty set holds
( X is categorial iff for x being Element of X holds x is Category );