theorem :: CLASSES5:97

for U being Universe
for C being b₁ -locally_small Category st the carrier of C is U -set holds
C is U -small