theorem Th29: :: REWRITE2:29

for E being set holds ==>.-relation ({} ((E ^omega),(E ^omega))) = {} ((E ^omega),(E ^omega))