let E, x be set ; :: thesis: for A being Subset of ()
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 (); :: 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
defpred S1[ 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 () : ex m being Nat st
( n <= m & B = A |^ m )
}
by TARSKI:def 4;
A3: X in { B where B is Subset of () : S1[B] } by A2;
S1[X] from CARD_FIL:sch 1(A3);
hence ex m being Nat st
( n <= m & x in A |^ m ) by A1; :: thesis: verum
end;
given m being Nat such that A4: n <= m and
A5: x in A |^ m ; :: thesis: x in A |^.. n
defpred S1[ set ] means ex m being Nat st
( n <= m & \$1 = A |^ m );
consider B being Subset of () such that
A6: x in B and
A7: S1[B] by A4, A5;
reconsider A = { C where C is Subset of () : S1[C] } as Subset-Family of () from B in A by A7;
hence x in A |^.. n by ; :: thesis: verum