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:]

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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in NonTerminals G ; :: thesis:
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:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A8: x in [:1,5:] ; :: thesis:
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:

end;

then A9: G is with_nonterminals by DTCONSTR:def 4;
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

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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Terminals G ; :: thesis:
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:
then t in [:1,5:] by A1, A12, XBOOLE_0:def 3;
then t ==> <*t,t*> by A2;
hence contradiction by A13; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A14: x in SCM-Data-Loc ; :: thesis:
then A15: ex y, z being object st
( y in {1} & z in NAT & x = [y,z] ) by ZFMISC_1:84;
reconsider t = x as Symbol of G by A1, A14, XBOOLE_0:def 3;
assume not x in Terminals G ; :: thesis:
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 object such that
A17: x1 in 1 and
x2 in 5 and
A18: x = [x1,x2] by ZFMISC_1:84;
x = [0,x2] by A17, A18, CARD_1:49, TARSKI:def 1;
hence contradiction by A15, XTUPLE_0:1; :: thesis:

end;

A19: dl. 1 in SCM-Data-Loc by AMI_2:def 16;
A20: dl. 0 in SCM-Data-Loc by AMI_2:def 16;
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 1;
root-tree d0 in TS G by A11, A20, DTCONSTR:def 1;
then reconsider p = <*(root-tree d0),(root-tree d1)*> as FinSequence of TS G by A21, FINSEQ_2:13;
let nt be Symbol of G; :: thesis:
assume A22: nt in NonTerminals G ; :: thesis:
take p = p; :: thesis:
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:

end;

then A23: G is with_useful_nonterminals by DTCONSTR:def 5;
G is with_terminals by A11, DTCONSTR:def 3;
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: