theorem Th16: :: LANG1:16

for D being non empty set holds Terminals (TotalGrammar D) = D