:: deftheorem Def10 defines the_empty_category ALTCAT_2:def 10 :
for b₁ being strict AltCatStr holds
( b₁ = the_empty_category iff the carrier of b₁ is empty );