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