theorem :: FLANG_2:18

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