:: deftheorem Def12 defines Chain ORDERS_2:def 12 :
for A being non empty Poset
for f being Choice_Function of (BOOL the carrier of A)
for b₃ being Chain of A holds
( b₃ is Chain of f iff ( b₃ <> {} & the InternalRel of A well_orders b₃ & ( for a being Element of A st a in b₃ holds
f . (UpperCone (InitSegm (b₃,a))) = a ) ) );