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