x -tree T1 = x -tree <*T1*> by TREES_4:def 5;
hence not x -tree T1 is trivial ; :: thesis: verum