theorem Th35: :: CAT_8:35

OrdC 1 is with_initial_objects