reconsider T = {{} } as Tree by TREES_1:48;
take T --> {} ; :: thesis: T --> {} is finite
thus T --> {} is finite ; :: thesis: verum