theorem :: FLANG_3:64
for E being set
for A being Subset of (E ^omega) holds
( A + = {(<%> E)} iff A = {(<%> E)} )