root-tree x = {[{} ,x]} by TREES_4:6;
hence root-tree x is finite ; :: thesis: verum