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