theorem Th50: :: REWRITE2:50

for E being set
for w being Element of E ^omega holds Lang (w,({} ((E ^omega),(E ^omega)))) = {w}