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