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