theorem :: LANG1:17

for D being non empty set holds Lang (TotalGrammar D) = D *