A2: ( rng (T | p) c= rng T & rng T c= D ) by Th34, RELAT_1:def 19;
A3: rng (T | p) c= D by A2, XBOOLE_1:1;
thus T | p is DecoratedTree of D by A3, RELAT_1:def 19; :: thesis: verum