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