reconsider 01 = {0 ,1} as non empty set ;
reconsider '0 = 0 , '1 = 1 as Element of 01 by TARSKI:def 2;
reconsider '11' = <*'1*> ^ <*'1*> as Element of 01 * ;
reconsider P = {['0,'11']} as Relation of 01,(01 * ) by RELSET_1:8;
take cherry = DTConstrStr(# 01,P #); :: thesis: ( cherry is binary & cherry is with_terminals & cherry is with_nonterminals & cherry is with_useful_nonterminals & cherry is strict )
reconsider '0 = '0, '1 = '1 as Symbol of cherry ;

hereby :: according to BINTREE1:def 4 :: thesis: ( cherry is with_terminals & cherry is with_nonterminals & cherry is with_useful_nonterminals & cherry is strict )

let s be Symbol of cherry; :: thesis: for p being FinSequence st s ==> p holds
ex x1, x2 being Symbol of cherry st p = <*x1,x2*>
let p be FinSequence; :: thesis: ( s ==> p implies ex x1, x2 being Symbol of cherry st p = <*x1,x2*> )
assume A1: s ==> p ; :: thesis: ex x1, x2 being Symbol of cherry st p = <*x1,x2*>
take x1 = '1; :: thesis: ex x2 being Symbol of cherry st p = <*x1,x2*>
take x2 = '1; :: thesis: p = <*x1,x2*>
[s,p] in P by A1, LANG1:def 1;
then [s,p] = [0 ,'11'] by TARSKI:def 1;
then p = '11' by ZFMISC_1:33
.= <*1,1*> by FINSEQ_1:def 9 ;
hence p = <*x1,x2*> ; :: thesis: verum

end;

now

let s be FinSequence; :: thesis: not '1 ==> s
assume '1 ==> s ; :: thesis: contradiction
then [1,s] in P by LANG1:def 1;
then [1,s] = [0 ,'11'] by TARSKI:def 1;
hence contradiction by ZFMISC_1:33; :: thesis: verum

end;

then A2: '1 in { t where t is Symbol of cherry : for s being FinSequence holds not t ==> s } ;
then A3: '1 in Terminals cherry by LANG1:def 2;
thus Terminals cherry <> {} by A2, LANG1:def 2; :: according to DTCONSTR:def 6 :: thesis: ( cherry is with_nonterminals & cherry is with_useful_nonterminals & cherry is strict )
['0,'11'] in P by TARSKI:def 1;
then '0 ==> '11' by LANG1:def 1;
then '0 in { t where t is Symbol of cherry : ex s being FinSequence st t ==> s } ;
hence NonTerminals cherry <> {} by LANG1:def 3; :: according to DTCONSTR:def 7 :: thesis: ( cherry is with_useful_nonterminals & cherry is strict )
A4: { s where s is Symbol of cherry : ex p being FinSequence st s ==> p } = NonTerminals cherry by LANG1:def 3;

hereby :: according to DTCONSTR:def 8 :: thesis: cherry is strict

reconsider X = TS cherry as non empty set by A3, DTCONSTR:def 4;
let nt be Symbol of cherry; :: thesis: ( nt in NonTerminals cherry implies ex q' being FinSequence of TS cherry st nt ==> roots q' )
reconsider rt1 = root-tree '1 as Element of X by A3, DTCONSTR:def 4;
reconsider q = <*rt1*> ^ <*rt1*> as FinSequence of TS cherry ;
q = <*(root-tree 1),(root-tree 1)*> by FINSEQ_1:def 9;
then A5: roots q = <*((root-tree '1) . {} ),((root-tree '1) . {} )*> by DTCONSTR:6;
assume nt in NonTerminals cherry ; :: thesis: ex q' being FinSequence of TS cherry st nt ==> roots q'
then ex s being Symbol of cherry st
( nt = s & ex p being FinSequence st s ==> p ) by A4;
then consider p being FinSequence such that
A6: nt ==> p ;
take q' = q; :: thesis: nt ==> roots q'
[nt,p] in P by A6, LANG1:def 1;
then A7: [nt,p] = [0 ,'11'] by TARSKI:def 1;
( '11' = <*1,1*> & (root-tree 1) . {} = 1 ) by FINSEQ_1:def 9, TREES_4:3;
hence nt ==> roots q' by A6, A7, A5, ZFMISC_1:33; :: thesis: verum

end;

thus cherry is strict ; :: thesis: verum