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