for E being non empty set
for u, v being Element of E ^omega st u <> v & u in Lex E & v in Lex E holds
for w being Element of E ^omega holds
( not u ^ w = v & not w ^ u = v )