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