theorem Th56: :: FLANG_3:56

for E being set
for A being Subset of (E ^omega) holds
( <%> E in A + iff <%> E in A )