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 s ==> p ; :: thesis: ex x1, x2 being Symbol of cherry st p = <*x1,x2*>
then [s,p] in P by LANG1:def 1;
then [s,p] = [0 ,'11'] by TARSKI:def 1;
then A1: p = '11' by ZFMISC_1:33
.= <*1,1*> by FINSEQ_1:def 9 ;
take x1 = '1; :: thesis: ex x2 being Symbol of cherry st p = <*x1,x2*>
take x2 = '1; :: thesis: p = <*x1,x2*>
thus p = <*x1,x2*> by A1; :: 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 A4: ( '0 in { t where t is Symbol of cherry : ex s being FinSequence st t ==> s } & { s where s is Symbol of cherry : ex p being FinSequence st s ==> p } = NonTerminals cherry ) by LANG1:def 3;
hence NonTerminals cherry <> {} ; :: according to DTCONSTR:def 7 :: thesis: ( cherry is with_useful_nonterminals & cherry is strict )

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

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

end;

thus cherry is strict ; :: thesis: verum