:: deftheorem defines tree TREES_3:def 17 :
for T1, T2 being Tree holds tree (T1,T2) = tree <*T1,T2*>;