set T = the Tree;
the Tree in Trees by Def1;
hence not Trees is empty ; :: thesis: verum