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