set W = the Tree;
take f = the Tree --> 0; :: thesis: f is DecoratedTree-like
thus dom f is Tree ; :: according to TREES_2:def 8 :: thesis: verum