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