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 |^ 1 c= A + by Th49;
hence A c= A + by FLANG_1:25; :: thesis: verum