for G being non empty DTConstrStr
for s being Symbol of G
for n being String of G st <*s*> ==> n holds
s ==> n