:: deftheorem Def8 defines Cartesian CAT_4:def 8 :
for IT being non empty non void Category-like transitive associative reflexive with_identities ProdCatStr holds
( IT is Cartesian iff ( the TerminalObj of IT is terminal & ( for a, b being Object of IT holds
( cod ( the Proj1 of IT . (a,b)) = a & cod ( the Proj2 of IT . (a,b)) = b & the CatProd of IT . (a,b) is_a_product_wrt the Proj1 of IT . (a,b), the Proj2 of IT . (a,b) ) ) ) );