theorem Th36: :: TREES_3:36

for x being object
for i being Nat st i <> 0 holds
( i |-> x is DTree-yielding iff x is DecoratedTree )