theorem Th61: :: CLASSES5:59

for U being Universe
for o, m being object holds 1Cat (o,m) is U -petit