theorem Th97: :: CLASSES5:95

for U being Universe
for o being object holds not 1Cat (o,U) is U -locally_small