c1Cat (0,1) is Cartesian by Th10;
hence ex b₁ being non empty non void Category-like transitive associative reflexive with_identities ProdCatStr st
( b₁ is strict & b₁ is Cartesian ) ; :: thesis: verum