theorem Th7: :: LANG1:7

for G being non empty DTConstrStr
for n, m being String of G st n ==> m holds
m is_derivable_from n