let E be set ; :: thesis: for A being Subset of (E ^omega) holds A ? c= A *
let A be Subset of (E ^omega); :: thesis: A ? c= A *
A ? = A |^ (0,1) by Th79;
hence A ? c= A * by Th32; :: thesis: verum