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