let E be set ; :: thesis: for B, A being Subset of (E ^omega ) st B c= A * holds
( (A * ) ^^ B c= A * & B ^^ (A * ) c= A * )
let B, A be Subset of (E ^omega ); :: thesis: ( B c= A * implies ( (A * ) ^^ B c= A * & B ^^ (A * ) c= A * ) )
assume B c= A * ; :: thesis: ( (A * ) ^^ B c= A * & B ^^ (A * ) c= A * )
then ( (A * ) ^^ B c= (A * ) ^^ (A * ) & B ^^ (A * ) c= (A * ) ^^ (A * ) ) by FLANG_1:18;
hence ( (A * ) ^^ B c= A * & B ^^ (A * ) c= A * ) by FLANG_1:64; :: thesis: verum