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 + )

A5: x in A |^ n ; :: thesis: x in A +

defpred S_{1}[ 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_{1}[B]
by A4, A5;

reconsider A = { C where C is Subset of (E ^omega) : S_{1}[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

( 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

given n being Nat such that A4:
n > 0
and
defpred S_{1}[ 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_{1}[B] }
by A2;

S_{1}[X]
from CARD_FIL:sch 1(A3);

hence ex n being Nat st

( n > 0 & x in A |^ n ) by A1; :: thesis: verum

end;( 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

S

hence ex n being Nat st

( n > 0 & x in A |^ n ) by A1; :: thesis: verum

A5: x in A |^ n ; :: thesis: x in A +

defpred S

( n > 0 & $1 = A |^ n );

consider B being Subset of (E ^omega) such that

A6: x in B and

A7: S

reconsider A = { C where C is Subset of (E ^omega) : S

B in A by A7;

hence x in A + by A6, TARSKI:def 4; :: thesis: verum