take {((elementary_tree 0) --> the Element of D)} ; :: thesis: for x being object st x in {((elementary_tree 0) --> the Element of D)} holds
x is DecoratedTree of D
thus for x being object st x in {((elementary_tree 0) --> the Element of D)} holds
x is DecoratedTree of D by TARSKI:def 1; :: thesis: verum