let E be set ; :: thesis: for A, B being Subset of (E ^omega) st <%> E in B holds
( A c= A ^^ (B +) & A c= (B +) ^^ A )
let A, B 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