T | p is D -valued

proof

( rng (T | p) c= rng T & rng T c= D ) by Th34, RELAT_1:def 19;
hence rng (T | p) c= D by XBOOLE_1:1; :: according to RELAT_1:def 19 :: thesis: verum

end;

hence T | p is DecoratedTree of ; :: thesis: verum