let t be DecoratedTree; :: thesis: ( t is finite-order implies t is finite-branching )
assume dom t is finite-order ; :: according to TREES_9:def 3 :: thesis: t is finite-branching
hence dom t is finite-branching ; :: according to TREES_9:def 4 :: thesis: verum