let E be set ; :: thesis: for A being Subset of (E ^omega )
for m, n being Nat holds A |^ m,n c= A *
let A be Subset of (E ^omega ); :: thesis: for m, n being Nat holds A |^ m,n c= A *
let m, n be Nat; :: thesis: A |^ m,n c= A *
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A |^ m,n or x in A * )
assume x in A |^ m,n ; :: thesis: x in A *
then ex k being Nat st
( m <= k & k <= n & x in A |^ k ) by Th19;
hence x in A * by FLANG_1:42; :: thesis: verum