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 A1: B c= A * ; :: thesis: ( (A * ) ^^ B c= A * & B ^^ (A * ) c= A * )
then A2: B ^^ (A * ) c= (A * ) ^^ (A * ) by FLANG_1:18;
(A * ) ^^ B c= (A * ) ^^ (A * ) by A1, FLANG_1:18;
hence ( (A * ) ^^ B c= A * & B ^^ (A * ) c= A * ) by A2, FLANG_1:64; :: thesis: verum