theorem Th60: :: TREES_3:60

for T being Tree
for x being object holds
( x in ^ T iff ( x = {} or ex p being FinSequence st
( p in T & x = <*0*> ^ p ) ) )