let E be set ; :: thesis: for A being Subset of (E ^omega) holds <%> E in A *
let A be Subset of (E ^omega); :: thesis: <%> E in A *
{(<%> E)} = A |^ 0 by Th25;
then <%> E in A |^ 0 by TARSKI:def 1;
hence <%> E in A * by Th42; :: thesis: verum