let E, x be set ; :: thesis: for A being Subset of (E ^omega ) holds
( x in A * iff ex n being Nat st x in A |^ n )
let A be Subset of (E ^omega ); :: thesis: ( x in A * iff ex n being Nat st x in A |^ n )
thus ( x in A * implies ex n being Nat st x in A |^ n ) :: thesis: ( ex n being Nat st x in A |^ n implies x in A * )

proof

assume x in A * ; :: thesis: ex n being Nat st x in A |^ n
then consider X being set such that
A1: x in X and
A2: X in { B where B is Subset of (E ^omega ) : ex k being Nat st B = A |^ k } by TARSKI:def 4;
defpred S₁[ set ] means ex k being Nat st $1 = A |^ k;
A3: X in { B where B is Subset of (E ^omega ) : S₁[B] } by A2;
S₁[X] from CARD_FIL:sch 1(A3);
hence ex n being Nat st x in A |^ n by A1; :: thesis: verum

end;

given n being Nat such that A4: x in A |^ n ; :: thesis: x in A *
defpred S₁[ set ] means ex k being Nat st $1 = A |^ k;
consider B being Subset of (E ^omega ) such that
A5: ( x in B & S₁[B] ) by A4;
reconsider A = { C where C is Subset of (E ^omega ) : S₁[C] } as Subset-Family of (E ^omega ) from DOMAIN_1:sch 7();
B in A by A5;
hence x in A * by A5, TARSKI:def 4; :: thesis: verum