theorem :: FLANG_3:73
for E being set
for A, B being Subset of (E ^omega) st <%> E in B holds
( A c= A ^^ (B +) & A c= (B +) ^^ A )