theorem Th94: :: CLASSES5:92

for U being Universe
for o, m being set st ( not m is U -set or not o is U -set ) holds
not 1Cat (o,m) is U -small