theorem Th68: :: TREES_3:68

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