theorem Th20: :: REWRITE2:20

for E being set
for s, t being Element of E ^omega holds not s ==>. t, {} ((E ^omega),(E ^omega))