the carrier of (IterGrammar a,b) = {a,b} by Def9;
hence not the carrier of (IterGrammar a,b) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum