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