:: deftheorem defines -Category CLASSES5:def 18 :
for U being Universe
for C being Category holds
( C is U -Category iff for x, y being Object of C holds Hom (x,y) is U -petit );