let x, y be set ; :: thesis: ( root-tree x = root-tree y implies x = y )
A1: (root-tree x) . {} = x by Th3;
thus ( root-tree x = root-tree y implies x = y ) by A1, Th3; :: thesis: verum