let E, x be set ; :: thesis: for A being Subset of (E ^omega)

for n being Nat holds

( x in A |^.. n iff ex m being Nat st

( n <= m & x in A |^ m ) )

let A be Subset of (E ^omega); :: thesis: for n being Nat holds

( x in A |^.. n iff ex m being Nat st

( n <= m & x in A |^ m ) )

let n be Nat; :: thesis: ( x in A |^.. n iff ex m being Nat st

( n <= m & x in A |^ m ) )

thus ( x in A |^.. n implies ex m being Nat st

( n <= m & x in A |^ m ) ) :: thesis: ( ex m being Nat st

( n <= m & x in A |^ m ) implies x in A |^.. n )

A5: x in A |^ m ; :: thesis: x in A |^.. n

defpred S_{1}[ set ] means ex m being Nat st

( n <= m & $1 = A |^ m );

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 |^.. n by A6, TARSKI:def 4; :: thesis: verum

for n being Nat holds

( x in A |^.. n iff ex m being Nat st

( n <= m & x in A |^ m ) )

let A be Subset of (E ^omega); :: thesis: for n being Nat holds

( x in A |^.. n iff ex m being Nat st

( n <= m & x in A |^ m ) )

let n be Nat; :: thesis: ( x in A |^.. n iff ex m being Nat st

( n <= m & x in A |^ m ) )

thus ( x in A |^.. n implies ex m being Nat st

( n <= m & x in A |^ m ) ) :: thesis: ( ex m being Nat st

( n <= m & x in A |^ m ) implies x in A |^.. n )

proof

given m being Nat such that A4:
n <= m
and
defpred S_{1}[ set ] means ex m being Nat st

( n <= m & $1 = A |^ m );

assume x in A |^.. n ; :: thesis: ex m being Nat st

( n <= m & x in A |^ m )

then consider X being set such that

A1: x in X and

A2: X in { B where B is Subset of (E ^omega) : ex m being Nat st

( n <= m & B = A |^ m ) } 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 m being Nat st

( n <= m & x in A |^ m ) by A1; :: thesis: verum

end;( n <= m & $1 = A |^ m );

assume x in A |^.. n ; :: thesis: ex m being Nat st

( n <= m & x in A |^ m )

then consider X being set such that

A1: x in X and

A2: X in { B where B is Subset of (E ^omega) : ex m being Nat st

( n <= m & B = A |^ m ) } by TARSKI:def 4;

A3: X in { B where B is Subset of (E ^omega) : S

S

hence ex m being Nat st

( n <= m & x in A |^ m ) by A1; :: thesis: verum

A5: x in A |^ m ; :: thesis: x in A |^.. n

defpred S

( n <= m & $1 = A |^ m );

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 |^.. n by A6, TARSKI:def 4; :: thesis: verum