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