theorem Th3: :: LANG1:3

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