theorem Th9: :: FLANG_2:9

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