:: deftheorem defines + FLANG_3:def 2 :
for E being set
for A being Subset of (E ^omega) holds A + = union { B where B is Subset of (E ^omega) : ex n being Nat st
( n > 0 & B = A |^ n ) } ;