let E be set ; :: thesis: for A being Subset of (E ^omega)
for n being Nat holds A |^.. n c= A *
let A be Subset of (E ^omega); :: thesis: for n being Nat holds A |^.. n c= A *
let n be Nat; :: thesis: A |^.. n c= A *

now

let x be set ; :: thesis: ( x in A |^.. n implies x in A * )
assume x in A |^.. n ; :: thesis: x in A *
then ex k being Nat st
( n <= k & x in A |^ k ) by Th2;
hence x in A * by FLANG_1:41; :: thesis: verum

end;

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