for E, x being set
for A being Subset of (E ^omega)
for n being Nat holds
( x in A |^.. n iff ex m being Nat st
( n <= m & x in A |^ m ) )