theorem Th48: :: FLANG_3:48

for E, x being set
for A being Subset of (E ^omega) holds
( x in A + iff ex n being Nat st
( n > 0 & x in A |^ n ) )