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 A2, Th9;
given w being Element of E ^omega such that A5: ( u ^ w = v or w ^ u = v ) ; :: thesis: contradiction
A6: len v = 1 by A3, Th9;
F: ( u ^ {} = u & {} ^ u = u ) ;

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 A4, AFINSQ_1:17;
then w = <%> E by A6, A7;
hence contradiction by A1, A7, F; :: thesis: verum

end;

suppose A8: w ^ u = v ; :: thesis: contradiction

len (w ^ u) = 1 + (len w) by A4, AFINSQ_1:17;
then w = <%> E by A6, A8;
hence contradiction by A1, A8, F; :: thesis: verum

end;

end;