theorem Th10: :: CAT_4:10

for o, m being set holds c1Cat (o,m) is Cartesian by Th8, Th3, Th9;