let E be set ; :: thesis: for A, B being Subset of (E ^omega) st B c= A * holds
( (A +) ^^ B c= A + & B ^^ (A +) c= A + )
let A, B 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:17;
then A2: B ^^ (A +) c= (A +) ^^ (A *) by Th86;
(A +) ^^ B c= (A +) ^^ (A *) by A1, FLANG_1:17;
hence ( (A +) ^^ B c= A + & B ^^ (A +) c= A + ) by A2, Th92; :: thesis: verum