c1Cat* (0,1) is Cocartesian by Th57;
hence ex b₁ being non empty non void Category-like CoprodCatStr st
( b₁ is strict & b₁ is Cocartesian ) ; :: thesis: verum