let x, y be set ; :: thesis: <:(root-tree x),(root-tree y):> = root-tree [x,y]
reconsider x' = x as Element of {x} by TARSKI:def 1;
reconsider y' = y as Element of {y} by TARSKI:def 1;
( (root-tree [x',y']) `1 = root-tree x & (root-tree [x',y']) `2 = root-tree y ) by Th25;
hence <:(root-tree x),(root-tree y):> = root-tree [x,y] by TREES_3:42; :: thesis: verum