theorem Th40: :: FLANG_3:40

for E being set
for A being Subset of (E ^omega)
for k being Nat holds
( A ? c= A |^.. k iff ( k = 0 or <%> E in A ) )