let t be DecoratedTree; :: thesis: ( t is root implies t is finite )
assume dom t = elementary_tree 0 ; :: according to TREES_9:def 1 :: thesis: t is finite
hence t is finite by FINSET_1:29; :: thesis: verum