for G being non empty with_terminals DTConstrStr
for tsg being Element of TS G
for s being Terminal of G st tsg . {} = s holds
tsg = root-tree s