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 * by Th64;
hence A ? c= B * by Th79; :: thesis: verum