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