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