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;
A1: ( (root-tree [x9,y9]) `1 = root-tree x & (root-tree [x9,y9]) `2 = root-tree y ) by Th25;
thus <:(root-tree x),(root-tree y):> = root-tree [x,y] by A1, TREES_3:42; :: thesis: verum