let E be set ; :: thesis: for A, B being Subset of (E ^omega ) holds
( A c= A ^^ (B ? ) & A c= (B ? ) ^^ A )
let A, B be Subset of (E ^omega ); :: thesis: ( A c= A ^^ (B ? ) & A c= (B ? ) ^^ A )
<%> E in B ? by Th78;
hence ( A c= A ^^ (B ? ) & A c= (B ? ) ^^ A ) by FLANG_1:17; :: thesis: verum