consider t being finite Tree;
take t ; :: thesis: t is finite
thus t is finite ; :: thesis: verum