theorem Th6: :: LANG1:6

for G being non empty DTConstrStr
for n being String of G holds n is_derivable_from n