theorem Th5: :: LANG1:5

for G being non empty DTConstrStr
for n, n1, n2 being String of G st n1 ==> n2 holds
( n ^ n1 ==> n ^ n2 & n1 ^ n ==> n2 ^ n )