theorem :: FLANG_3:93

for E being set
for A, B being Subset of (E ^omega) st B c= A * holds
( (A +) ^^ B c= A + & B ^^ (A +) c= A + )