set T = LexOrder n;
take LexOrder n ; :: thesis: ( LexOrder n is admissible & LexOrder n is connected )

now :: thesis: for x, y being object st x in field (LexOrder n) & y in field (LexOrder n) & x <> y & not [x,y] in LexOrder n holds
[y,x] in LexOrder n

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

end;

then LexOrder n is_connected_in field (LexOrder n) by RELAT_2:def 6;
hence ( LexOrder n is admissible & LexOrder n is connected ) by RELAT_2:def 14; :: thesis: verum