theorem Th47: :: CAT_8:47

for C1, C2 being category holds (C1 ->OrdC1) [|x|] (C2 ->OrdC1), pr1 ((C1 ->OrdC1),(C2 ->OrdC1)), pr2 ((C1 ->OrdC1),(C2 ->OrdC1)) is_product_of C1,C2