the carrier of (EmptyGrammar a) = {a} by Def7;
hence not the carrier of (EmptyGrammar a) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum