theorem :: TREES_4:26

for x, y being set holds <:(root-tree x),(root-tree y):> = root-tree [x,y]