reconsider
r
=
{}
as
Node
of
t
by
TREES_1:22
;
t
.
r
is
Element
of
D
;
hence
t
.
{}
is
Element
of
D
;
:: thesis:
verum