theorem Th17: :: TREES_3:17

for x, y being object holds
( {x,y} is constituted-DTrees iff ( x is DecoratedTree & y is DecoratedTree ) )