theorem :: CLASSES5:89

for U being Universe
for C being strict Category holds
( C is U -petit iff CatToSet C is U -petit )