defpred S₁[ set , set , set ] means $1 in [:1,5:];
consider G being non empty strict binary DTConstrStr such that
A1: the carrier of G = SCM-Data-Loc \/ [:1,5:] and
A2: for x, y, z being Symbol of G holds
( x ==> <*y,z*> iff S₁[x,y,z] ) from BINTREE1:sch 1();
A3: Terminals G = { t where t is Symbol of G : for tnt being FinSequence holds not t ==> tnt } by LANG1:def 2;
A4: Terminals G = SCM-Data-Loc

proof

thus Terminals G c= SCM-Data-Loc :: according to XBOOLE_0:def 10 :: thesis: SCM-Data-Loc c= Terminals G

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Terminals G or x in SCM-Data-Loc )
assume x in Terminals G ; :: thesis: x in SCM-Data-Loc
then consider t being Symbol of G such that
A5: ( x = t & ( for tnt being FinSequence holds not t ==> tnt ) ) by A3;
assume not x in SCM-Data-Loc ; :: thesis: contradiction
then t in [:1,5:] by A1, A5, XBOOLE_0:def 3;
then t ==> <*t,t*> by A2;
hence contradiction by A5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in SCM-Data-Loc or x in Terminals G )
assume A6: x in SCM-Data-Loc ; :: thesis: x in Terminals G
then reconsider t = x as Symbol of G by A1, XBOOLE_0:def 3;
assume not x in Terminals G ; :: thesis: contradiction
then consider tnt being FinSequence such that
A7: t ==> tnt by A3;
consider x1, x2 being Symbol of G such that
A8: tnt = <*x1,x2*> by A7, BINTREE1:def 4;
consider y, z being set such that
A9: y in {1} and
z in NAT and
A11: x = [y,z] by A6, ZFMISC_1:103;
A12: y = 1 by A9, TARSKI:def 1;
x in [:1,5:] by A2, A7, A8;
then consider x1, x2 being set such that
A13: ( x1 in 1 & x2 in 5 & x = [x1,x2] ) by ZFMISC_1:103;
x = [0 ,x2] by A13, CARD_1:87, TARSKI:def 1;
hence contradiction by A11, A12, ZFMISC_1:33; :: thesis: verum

end;

A14: NonTerminals G = { t where t is Symbol of G : ex tnt being FinSequence st t ==> tnt } by LANG1:def 3;
A15: NonTerminals G = [:1,5:]

proof

thus NonTerminals G c= [:1,5:] :: according to XBOOLE_0:def 10 :: thesis: [:1,5:] c= NonTerminals G

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in NonTerminals G or x in [:1,5:] )
assume x in NonTerminals G ; :: thesis: x in [:1,5:]
then consider t being Symbol of G such that
A16: ( x = t & ex tnt being FinSequence st t ==> tnt ) by A14;
consider tnt being FinSequence such that
A17: t ==> tnt by A16;
consider x1, x2 being Symbol of G such that
A18: tnt = <*x1,x2*> by A17, BINTREE1:def 4;
thus x in [:1,5:] by A2, A16, A17, A18; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [:1,5:] or x in NonTerminals G )
assume A19: x in [:1,5:] ; :: thesis: x in NonTerminals G
then reconsider t = x as Symbol of G by A1, XBOOLE_0:def 3;
t ==> <*t,t*> by A2, A19;
hence x in NonTerminals G by A14; :: thesis: verum

end;

A20: G is with_terminals by A4, DTCONSTR:def 6;
A21: G is with_nonterminals by A15, DTCONSTR:def 7;

now

let nt be Symbol of G; :: thesis: ( nt in NonTerminals G implies ex p being FinSequence of TS G st nt ==> roots p )
assume A22: nt in NonTerminals G ; :: thesis: ex p being FinSequence of TS G st nt ==> roots p
A23: ( dl. 0 in SCM-Data-Loc & dl. 1 in SCM-Data-Loc ) by AMI_3:def 2;
then reconsider d0 = dl. 0 , d1 = dl. 1 as Symbol of G by A1, XBOOLE_0:def 3;
( root-tree d0 in TS G & root-tree d1 in TS G ) by A4, A23, DTCONSTR:def 4;
then reconsider p = <*(root-tree d0),(root-tree d1)*> as FinSequence of TS G by FINSEQ_2:15;
A24: roots p = <*((root-tree d0) . {} ),((root-tree d1) . {} )*> by DTCONSTR:6
.= <*((root-tree d0) . {} ),d1*> by TREES_4:3
.= <*d0,d1*> by TREES_4:3 ;
take p = p; :: thesis: nt ==> roots p
thus nt ==> roots p by A2, A15, A22, A24; :: thesis: verum

end;

then G is with_useful_nonterminals by DTCONSTR:def 8;
hence ex b₁ being non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr st
( Terminals b₁ = SCM-Data-Loc & NonTerminals b₁ = [:1,5:] & ( for x, y, z being Symbol of b₁ holds
( x ==> <*y,z*> iff x in [:1,5:] ) ) ) by A2, A4, A15, A20, A21; :: thesis: verum