theorem :: CLASSES5:64

for U being Universe
for C being strict Category st C is U -element holds
C is U -petit ;