theorem Th27: :: REWRITE2:27

for E being set holds ==>.-relation (id (E ^omega)) = id (E ^omega)