theorem Th61: :: TREES_3:61

for T being Tree
for p being FinSequence holds
( p in T iff <*0*> ^ p in ^ T )