:: deftheorem defines |^.. FLANG_3:def 1 :
for E being set
for A being Subset of (E ^omega)
for n being Nat holds A |^.. n = union { B where B is Subset of (E ^omega) : ex m being Nat st
( n <= m & B = A |^ m ) } ;