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: NonTerminals G = { t where t is Symbol of G : ex tnt being FinSequence st t ==> tnt } by LANG1:def 3;
A4: 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
A5: x = t and
A6: ex tnt being FinSequence st t ==> tnt by A3;
consider tnt being FinSequence such that
A7: t ==> tnt by A6;
ex x1, x2 being Symbol of G st tnt = <*x1,x2*> by A7, BINTREE1:def 4;
hence x in [:1,5:] by A2, A5, A7; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [:1,5:] or x in NonTerminals G )
assume A8: 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, A8;
hence x in NonTerminals G by A3; :: thesis: verum

end;

then A9: G is with_nonterminals by DTCONSTR:def 7;
A10: Terminals G = { t where t is Symbol of G : for tnt being FinSequence holds not t ==> tnt } by LANG1:def 2;
A11: 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
A12: x = t and
A13: for tnt being FinSequence holds not t ==> tnt by A10;
assume not x in SCM-Data-Loc ; :: thesis: contradiction
then t in [:1,5:] by A1, A12, XBOOLE_0:def 3;
then t ==> <*t,t*> by A2;
hence contradiction by A13; :: 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 A14: x in SCM-Data-Loc ; :: thesis: x in Terminals G
then A15: ex y, z being set st
( y in {1} & z in NAT & x = [y,z] ) by ZFMISC_1:103;
reconsider t = x as Symbol of G by A1, A14, XBOOLE_0:def 3;
assume not x in Terminals G ; :: thesis: contradiction
then consider tnt being FinSequence such that
A16: t ==> tnt by A10;
ex x1, x2 being Symbol of G st tnt = <*x1,x2*> by A16, BINTREE1:def 4;
then x in [:1,5:] by A2, A16;
then consider x1, x2 being set such that
A17: x1 in 1 and
x2 in 5 and
A18: x = [x1,x2] by ZFMISC_1:103;
x = [0 ,x2] by A17, A18, CARD_1:87, TARSKI:def 1;
hence contradiction by A15, ZFMISC_1:33; :: thesis: verum

end;

now

A19: dl. 1 in SCM-Data-Loc by AMI_3:def 2;
A20: dl. 0 in SCM-Data-Loc by AMI_3:def 2;
then reconsider d0 = dl. 0 , d1 = dl. 1 as Symbol of G by A1, A19, XBOOLE_0:def 3;
A21: root-tree d1 in TS G by A11, A19, DTCONSTR:def 4;
root-tree d0 in TS G by A11, A20, DTCONSTR:def 4;
then reconsider p = <*(root-tree d0),(root-tree d1)*> as FinSequence of TS G by A21, FINSEQ_2:15;
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
take p = p; :: thesis: nt ==> roots p
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 ;
hence nt ==> roots p by A2, A4, A22; :: thesis: verum

end;

then A23: G is with_useful_nonterminals by DTCONSTR:def 8;
G is with_terminals by A11, DTCONSTR:def 6;
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, A11, A4, A9, A23; :: thesis: verum