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