set T = the finite Tree;
set t = the Function of the finite Tree,D;
dom the Function of the finite Tree,D is finite ;
hence not FinTrees D is empty by Def8; :: thesis: verum