let E be set ; :: thesis: for A being Subset of (E ^omega ) holds A ^^ A c= A *
let A be Subset of (E ^omega ); :: thesis: A ^^ A c= A *
A ^^ A = A |^ 2 by Th27;
hence A ^^ A c= A * by Th43; :: thesis: verum