let E be non empty set ; :: thesis: 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 )

let u, v be Element of E ^omega ; :: thesis: ( u <> v & u in Lex E & v in Lex E implies for w being Element of E ^omega holds
( not u ^ w = v & not w ^ u = v ) )

assume that
A1: u <> v and
A2: u in Lex E and
A3: v in Lex E ; :: thesis: for w being Element of E ^omega holds
( not u ^ w = v & not w ^ u = v )

A4: len u = 1 by ;
given w being Element of E ^omega such that A5: ( u ^ w = v or w ^ u = v ) ; :: thesis: contradiction
A6: len v = 1 by ;
per cases ( u ^ w = v or w ^ u = v ) by A5;
suppose A7: u ^ w = v ; :: thesis: contradiction
len (u ^ w) = 1 + (len w) by ;
then w = <%> E by A6, A7;
hence contradiction by A1, A7; :: thesis: verum
end;
suppose A8: w ^ u = v ; :: thesis: contradiction
len (w ^ u) = 1 + (len w) by ;
then w = <%> E by A6, A8;
hence contradiction by A1, A8; :: thesis: verum
end;
end;