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