:: deftheorem defines -tree TREES_4:def 6 :
for x being object
for T1, T2 being DecoratedTree holds x -tree (T1,T2) = x -tree <*T1,T2*>;