theorem :: FLANG_1:75

for E being set
for A being Subset of (E ^omega) st A * = E ^omega holds
Lex E c= A