let E be set ; :: thesis: for A being Subset of (E ^omega ) holds (A ? ) ? = A ?
let A be Subset of (E ^omega ); :: thesis: (A ? ) ? = A ?
<%> E in A ? by Th78;
hence (A ? ) ? = A ? by Th80; :: thesis: verum