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 A1: A c= B ; :: thesis: A * c= B *
B c= B * by Th43;
then A c= B * by A1;
hence A * c= B * by Th60; :: thesis: verum