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

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