consider T being Tree;
T in Trees by Def1;
hence not Trees is empty ; :: thesis: verum