:: deftheorem defines TerminalLanguage DTCONSTR:def 14 :
for G being non empty with_nonterminals DTConstrStr
for nt being Symbol of G holds TerminalLanguage nt = { (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ;