:: deftheorem defines * FLANG_1:def 3 :
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 B = A |^ n } ;