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