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