dom (x -tree p) = tree (doms p) by TREES_4:10;
hence x -tree p is finite by FINSET_1:10; :: thesis: verum