set d = the Element of D;
reconsider T = {{}} as Tree by TREES_1:48;
take T --> the Element of D ; :: thesis: T --> the Element of D is finite
thus T --> the Element of D is finite ; :: thesis: verum