theorem :: TREES_3:58

for T being Tree holds ^ T = (elementary_tree 1) with-replacement (<*0*>,T)