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

proof

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

end;

thus A ^^ (A * ) c= A * :: thesis: verum

proof

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

end;