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