let x, y be object ; :: thesis: ( x in field (LexOrder n) & y in field (LexOrder n) & x <> y & not [x,y] in LexOrder n implies [y,x] in LexOrder n )
assume that
A1: ( x in field (LexOrder n) & y in field (LexOrder n) ) and
x <> y ; :: thesis: ( [x,y] in LexOrder n or [y,x] in LexOrder n )
reconsider b1 = x, b2 = y as bag of n by A1, Lm1;
( b1 <=' b2 or b2 <=' b1 ) by PRE_POLY:45;
hence ( [x,y] in LexOrder n or [y,x] in LexOrder n ) by PRE_POLY:def 14; :: thesis: verum