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