let E be set ; :: thesis: for A being Subset of (E ^omega)
for n being Nat st n > 0 holds
A |^.. n c= A +
let A be Subset of (E ^omega); :: thesis: for n being Nat st n > 0 holds
A |^.. n c= A +
let n be Nat; :: thesis: ( n > 0 implies A |^.. n c= A + )
assume A1: n > 0 ; :: 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
( k >= n & x in A |^ k ) by Th2;
hence x in A + by A1, Th48; :: thesis: verum