branchdeg v = card (succ v) by TREES_2:def 12;
hence branchdeg v is Element of NAT ; :: thesis: verum