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