let E be set ; :: thesis: for A being Subset of (E ^omega)
for m being Nat holds
( A |^ (m + 1) c= (A *) ^^ A & A |^ (m + 1) c= A ^^ (A *) )
let A be Subset of (E ^omega); :: thesis: for m being Nat holds
( A |^ (m + 1) c= (A *) ^^ A & A |^ (m + 1) c= A ^^ (A *) )
let m be Nat; :: thesis: ( A |^ (m + 1) c= (A *) ^^ A & A |^ (m + 1) c= A ^^ (A *) )
thus A |^ (m + 1) c= (A *) ^^ A :: thesis: A |^ (m + 1) c= A ^^ (A *)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A |^ (m + 1) or x in (A *) ^^ A )
assume x in A |^ (m + 1) ; :: thesis: x in (A *) ^^ A
hence x in (A *) ^^ A by Th51; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A |^ (m + 1) or x in A ^^ (A *) )
assume x in A |^ (m + 1) ; :: thesis: x in A ^^ (A *)
hence x in A ^^ (A *) by Th51; :: thesis: verum