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