theorem :: FLANG_1:47

for E being set
for A being Subset of (E ^omega) holds
( A * = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) )