theorem Th12: :: LANG1:12

for a, b being set st a <> b holds
Terminals (SingleGrammar (a,b)) = {b}