theorem :: ALTCAT_2:19

for E being empty strict AltCatStr holds E = the_empty_category by Lm1;