for E being set
for a being Element of E ^omega holds a in (Lex E) |^ (len a)