theorem Th41: :: CAT_8:41

OrdC 1 is with_binary_products