theorem Th96: :: CLASSES5:94

for U being Universe
for C being b₁ -small Category holds C is U -locally_small