theorem Th34: :: TREES_3:34

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