let E be set ; :: thesis: for A being Subset of (E ^omega )
for k, m, n being Nat st k <= m holds
A |^ m,n c= A |^.. k
let A be Subset of (E ^omega ); :: thesis: for k, m, n being Nat st k <= m holds
A |^ m,n c= A |^.. k
let k, m, n be Nat; :: thesis: ( k <= m implies A |^ m,n c= A |^.. k )
assume A1: k <= m ; :: thesis: A |^ m,n c= A |^.. k

now

let x be set ; :: thesis: ( x in A |^ m,n implies x in A |^.. k )
assume x in A |^ m,n ; :: thesis: x in A |^.. k
then consider l being Nat such that
A2: ( m <= l & l <= n & x in A |^ l ) by FLANG_2:19;
k <= l by A1, A2, XXREAL_0:2;
hence x in A |^.. k by A2, Th2; :: thesis: verum

end;

hence A |^ m,n c= A |^.. k by TARSKI:def 3; :: thesis: verum