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 *

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A |^.. n or 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

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 *

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A |^.. n or 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