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;