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:70, TREES_4:3 ;
hence t is finite by FINSET_1:29; :: 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 )*> by TREES_4:def 5 ;
hence contradiction by TREES_4:17; :: thesis: verum