:: deftheorem defines -petit CLASSES5:def 17 :
for U being Universe
for C being Category holds
( C is U -petit iff ex c being strict Category st
( c is U -element & C ~= c ) );