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
A1: x in minimals R and
A2: y in minimals R and
A3: x <> y ; :: thesis: ( not x <= y & not y <= x )
A4: not R is empty by A1;
then y is_minimal_in [#] R by A2, Def9;
then not y > x by A1, WAYBEL_4:56;
hence not x <= y by A3; :: thesis: not y <= x
x is_minimal_in [#] R by A1, A4, Def9;
then not x > y by A2, WAYBEL_4:56;
hence not y <= x by A3; :: thesis: verum