:: deftheorem Def7 defines Branch-like TREES_2:def 7 :
for W being Tree
for IT being Chain of W holds
( IT is Branch-like iff ( ( for p being FinSequence of NAT st p in IT holds
ProperPrefixes p c= IT ) & ( for p being FinSequence of NAT holds
( not p in W or ex q being FinSequence of NAT st
( q in IT & not q is_a_proper_prefix_of p ) ) ) ) );