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