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