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