theorem Th73: :: FLANG_2:73

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