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
A5: x in maximals R and
A6: y in maximals R and
A7: x <> y ; :: thesis: ( not x <= y & not y <= x )
A8: not R is empty by A5;
then x is_maximal_in [#] R by A5, Def10;
then not y > x by A6, WAYBEL_4:55;
hence not x <= y by A7; :: thesis: not y <= x
y is_maximal_in [#] R by A6, A8, Def10;
then not x > y by A5, WAYBEL_4:55;
hence not y <= x by A7; :: thesis: verum