the carrier of (TotalGrammar D) = succ D by Def10;
hence not the carrier of (TotalGrammar D) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum