theorem :: FLANG_3:81

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