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