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