x -tree (T1,T2) = x -tree <*T1,T2*> by TREES_4:def 6;
hence not x -tree (T1,T2) is trivial ; :: thesis: verum