let t be Tree; :: thesis: ( t is finite-order implies t is finite-branching )
assume t is finite-order ; :: thesis: t is finite-branching
then reconsider a = t as finite-order Tree ;
let x be Element of t; :: according to TREES_9:def 2 :: thesis: succ x is finite
reconsider x = x as Element of a ;
succ x is finite ;
hence succ x is finite ; :: thesis: verum