let G be non empty with_terminals with_nonterminals binary DTConstrStr ; :: thesis: 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 = <*(),()*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )

let ts be FinSequence of TS G; :: thesis: 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 = <*(),()*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )

let nt be Symbol of G; :: thesis: ( nt ==> roots ts implies ( 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 = <*(),()*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) ) )

assume A1: nt ==> roots ts ; :: thesis: ( 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 = <*(),()*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )

then consider rtl, rtr being Symbol of G such that
A2: roots ts = <*rtl,rtr*> by Def4;
nt in { s where s is Symbol of G : ex rts being FinSequence st s ==> rts } by A1;
hence nt is NonTerminal of G by LANG1:def 3; :: thesis: ( dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st
( roots ts = <*(),()*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )

A3: len <*rtl,rtr*> = 2 by FINSEQ_1:44;
A4: dom <*rtl,rtr*> = dom ts by ;
hence dom ts = {1,2} by ; :: thesis: ( 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st
( roots ts = <*(),()*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )

hence A5: ( 1 in dom ts & 2 in dom ts ) by TARSKI:def 2; :: thesis: ex tl, tr being Element of TS G st
( roots ts = <*(),()*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts )

then consider tl being DecoratedTree such that
A6: tl = ts . 1 and
A7: <*rtl,rtr*> . 1 = tl . {} by ;
A8: ( rng ts c= TS G & tl in rng ts ) by ;
consider tr being DecoratedTree such that
A9: tr = ts . 2 and
A10: <*rtl,rtr*> . 2 = tr . {} by ;
tr in rng ts by ;
then reconsider tl = tl, tr = tr as Element of TS G by A8;
take tl ; :: thesis: ex tr being Element of TS G st
( roots ts = <*(),()*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts )

take tr ; :: thesis: ( roots ts = <*(),()*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts )
<*rtl,rtr*> . 1 = rtl by FINSEQ_1:44;
hence roots ts = <*(),()*> by ; :: thesis: ( tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts )
Seg (len <*rtl,rtr*>) = dom <*rtl,rtr*> by FINSEQ_1:def 3
.= Seg (len ts) by ;
then len ts = 2 by ;
then ts = <*tl,tr*> by ;
hence ( tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) ) by ; :: thesis: ( tl in rng ts & tr in rng ts )
thus ( tl in rng ts & tr in rng ts ) by ; :: thesis: verum