:: deftheorem Def13 defines Chains ORDERS_2:def 13 :
for A being non empty Poset
for f being Choice_Function of (BOOL the carrier of A)
for b₃ being set holds
( b₃ = Chains f iff for x being set holds
( x in b₃ iff x is Chain of f ) );