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

proof

defpred S₁[ set ] means ex n being Nat st
( n > 0 & $1 = A |^ n );
assume x in A + ; :: thesis: ex n being Nat st
( n > 0 & 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 n being Nat st
( n > 0 & B = A |^ n ) } by TARSKI:def 4;
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
( n > 0 & x in A |^ n ) by A1; :: thesis: verum

end;

given n being Nat such that A4: n > 0 and
A5: x in A |^ n ; :: thesis: x in A +
defpred S₁[ set ] means ex n being Nat st
( n > 0 & $1 = A |^ n );
consider B being Subset of (E ^omega) such that
A6: x in B and
A7: S₁[B] by A4, A5;
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 A7;
hence x in A + by A6, TARSKI:def 4; :: thesis: verum