let E be set ; :: thesis: for A being Subset of (E ^omega )
for m, k, n being Nat st m <= k & k <= n holds
A |^ k c= A |^ m,n
let A be Subset of (E ^omega ); :: thesis: for m, k, n being Nat st m <= k & k <= n holds
A |^ k c= A |^ m,n
let m, k, n be Nat; :: thesis: ( m <= k & k <= n implies A |^ k c= A |^ m,n )
assume ( m <= k & k <= n ) ; :: thesis: A |^ k c= A |^ m,n
then for x being set st x in A |^ k holds
x in A |^ m,n by Th19;
hence A |^ k c= A |^ m,n by TARSKI:def 3; :: thesis: verum