theorem Th70: :: TREES_3:70

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