theorem Th69: :: TREES_3:69

for T1, T2 being Tree
for p being FinSequence holds
( p in T1 iff <*0*> ^ p in tree (T1,T2) )