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 Th24;
then <%> E in A |^ 0 by TARSKI:def 1;
hence <%> E in A * by Th41; :: thesis: verum