set mR = maximals R;
let x, y be Element of R; :: according to DILWORTH:def 2 :: thesis: ( x in maximals R & y in maximals R & x <> y implies ( not x <= y & not y <= x ) )
assume that
A: x in maximals R and
B: y in maximals R and
C: x <> y ; :: thesis: ( not x <= y & not y <= x )
D: not R is empty by A;
then x is_maximal_in [#] R by A, Lmax;
then not y > x by B, WAYBEL_4:56;
hence not x <= y by C, ORDERS_2:def 10; :: thesis: not y <= x
y is_maximal_in [#] R by B, D, Lmax;
then not x > y by A, WAYBEL_4:56;
hence not y <= x by C, ORDERS_2:def 10; :: thesis: verum