:: deftheorem Def9 defines minimals DILWORTH:def 9 :
for R being RelStr
for b₂ being Subset of R holds
( ( not R is empty implies ( b₂ = minimals R iff for x being Element of R holds
( x in b₂ iff x is_minimal_in [#] R ) ) ) & ( R is empty implies ( b₂ = minimals R iff b₂ = {} ) ) );