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;

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;