theorem Th2: :: FLANG_3:2

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 ) )