:: deftheorem Def3 defines Chain TREES_2:def 3 :
for W being Tree
for b₂ being Subset of W holds
( b₂ is Chain of W iff for p, q being FinSequence of NAT st p in b₂ & q in b₂ holds
p,q are_c=-comparable );