set T = the finite Tree;
the finite Tree in FinTrees by Def2;
hence not FinTrees is empty ; :: thesis: verum