take t = 0 -tree (root-tree 0); :: thesis: ( t is finite & not t is root )
dom t = ^ (dom (root-tree 0)) by TREES_4:13
.= elementary_tree 1 by TREES_3:67, TREES_4:3 ;
hence t is finite by FINSET_1:10; :: thesis: not t is root
assume dom t = elementary_tree 0 ; :: according to TREES_9:def 1 :: thesis: contradiction
then root-tree (t . {}) = t by TREES_4:5
.= 0 -tree <*(root-tree 0)*> ;
hence contradiction by TREES_4:17; :: thesis: verum