theorem Th50: :: FLANG_1:50

for E, x being set
for A being Subset of (E ^omega)
for m being Nat st x in A |^ (m + 1) holds
( x in (A *) ^^ A & x in A ^^ (A *) )