theorem Th10: :: BINTREE1:10

for G being non empty with_terminals with_nonterminals binary DTConstrStr
for ts being FinSequence of TS G
for nt being Symbol of G st nt ==> roots ts holds
( nt is NonTerminal of G & dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st
( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )