let E be set ; :: thesis: for A being Subset of (E ^omega )
for k being Nat holds (A |^ k) ? c= A *
let A be Subset of (E ^omega ); :: thesis: for k being Nat holds (A |^ k) ? c= A *
let k be Nat; :: thesis: (A |^ k) ? c= A *
(A |^ k) ? = (A |^ k) |^ 0 ,1 by Th79;
hence (A |^ k) ? c= A * by Th69; :: thesis: verum