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