theorem :: FLANG_2:13

for E being set
for A, B being Subset of (E ^omega)
for l being Nat st <%> E in B holds
( A c= A ^^ (B |^ l) & A c= (B |^ l) ^^ A )