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

now

let x, y be set ; :: 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 ( x in field (LexOrder n) & y in field (LexOrder n) & x <> y ) ; :: thesis: ( [x,y] in LexOrder n or [y,x] in LexOrder n )
then reconsider b1 = x, b2 = y as bag of by Lm1;
( b1 <=' b2 or b2 <=' b1 ) by POLYNOM1:49;
hence ( [x,y] in LexOrder n or [y,x] in LexOrder n ) by POLYNOM1:def 16; :: 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