theorem :: LANG1:13

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