theorem Th46: :: FLANG_3:46

for E, x being set
for A being Subset of (E ^omega)
for k being Nat holds
( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) )