theorem Th19: :: FLANG_2:19

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