theorem :: TREES_3:59

for T1, T2 being Tree holds tree (T1,T2) = ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2)