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:16; :: thesis: verum