consider T being finite Tree;
T in FinTrees by Def2;
hence not FinTrees is empty ; :: thesis: verum