theorem Th7: :: BINTREE1:7

for T0, T1 being Tree
for t being Element of tree (T0,T1) holds
( ( t = {} implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) & ( for p being Element of T0 st t = <*0*> ^ p holds
for sp being FinSequence holds
( sp in succ p iff <*0*> ^ sp in succ t ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds
for sp being FinSequence holds
( sp in succ p iff <*1*> ^ sp in succ t ) ) )