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 ? )
<%> E in B ? by Th78;
then A1: {(<%> E)} c= B ? by ZFMISC_1:31;
assume A c= B ? ; :: thesis: A ? c= B ?
then {(<%> E)} \/ A c= B ? by A1, XBOOLE_1:8;
hence A ? c= B ? by Th76; :: thesis: verum