let E be set ; :: thesis: for A, B being Subset of (E ^omega) st A c= B holds
A ? c= B ?
let A, B be Subset of (E ^omega); :: thesis: ( A c= B implies A ? c= B ? )
assume A c= B ; :: thesis: A ? c= B ?
then A |^ (0,1) c= B |^ (0,1) by Th29;
then A ? c= B |^ (0,1) by Th79;
hence A ? c= B ? by Th79; :: thesis: verum