theorem Th57: :: FLANG_3:57

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