:: deftheorem defines branchdeg TREES_2:def 12 :
for Tr being finite Tree
for v being Element of Tr holds branchdeg v = card (succ v);