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