theorem Th27: :: TREES_3:27

for p, q being FinSequence holds
( ( p is DTree-yielding & q is DTree-yielding ) iff p ^ q is DTree-yielding )