theorem :: FLANG_3:96

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