A1: W --> d is DecoratedTree ;
thus W --> d is DecoratedTree of D by A1; :: thesis: verum