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