let E be set ; :: thesis: for B, A being Subset of (E ^omega ) st <%> E in B holds
( A c= A ^^ (B + ) & A c= (B + ) ^^ A )
let B, A be Subset of (E ^omega ); :: thesis: ( <%> E in B implies ( A c= A ^^ (B + ) & A c= (B + ) ^^ A ) )
assume <%> E in B ; :: thesis: ( A c= A ^^ (B + ) & A c= (B + ) ^^ A )
then B + = B * by Th57;
hence ( A c= A ^^ (B + ) & A c= (B + ) ^^ A ) by FLANG_2:18; :: thesis: verum