theorem Th69: :: CAT_8:69

OrdC 1 is with_exponential_objects