take t = root-tree 0; :: thesis: t is root
thus dom t = elementary_tree 0 by TREES_4:3; :: according to TREES_9:def 1 :: thesis: verum