theorem Th16: :: FLANG_1:16
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 )