dom (d -tree p) = tree (doms p) by Th10;
hence d -tree p is Element of FinTrees D by TREES_3:def 8; :: thesis: verum