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

proof

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

end;

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