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 FLANG_1:48;
hence ( A c= A ^^ (B *) & A c= (B *) ^^ A ) by FLANG_1:16; :: thesis: verum