reconsider 01 = {0,1} as non empty set ;
reconsider a90 = 0 , a91 = 1 as Element of 01 by TARSKI:def 2;
reconsider a9119 = <*a91*> ^ <*a91*> as Element of 01 * ;
reconsider P = {[a90,a9119]} as Relation of 01,(01 *) ;
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 a90 = a90, a91 = a91 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 = a91; :: thesis: ex x2 being Symbol of cherry st p = <*x1,x2*>
take x2 = a91; :: thesis: p = <*x1,x2*>
[s,p] in P by A1, LANG1:def 1;
then [s,p] = [0,a9119] by TARSKI:def 1;
then p = a9119 by XTUPLE_0:1
.= <*1,1*> by FINSEQ_1:def 9 ;
hence p = <*x1,x2*> ; :: thesis: verum

end;

now :: thesis: for s being FinSequence holds not a91 ==> s

let s be FinSequence; :: thesis: not a91 ==> s
assume a91 ==> s ; :: thesis: contradiction
then [1,s] in P by LANG1:def 1;
then [1,s] = [0,a9119] by TARSKI:def 1;
hence contradiction by XTUPLE_0:1; :: thesis: verum

end;

then A2: a91 in { t where t is Symbol of cherry : for s being FinSequence holds not t ==> s } ;
then A3: a91 in Terminals cherry by LANG1:def 2;
thus Terminals cherry <> {} by A2, LANG1:def 2; :: according to DTCONSTR:def 3 :: thesis: ( cherry is with_nonterminals & cherry is with_useful_nonterminals & cherry is strict )
[a90,a9119] in P by TARSKI:def 1;
then a90 ==> a9119 by LANG1:def 1;
then a90 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 4 :: 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 5 :: thesis: cherry is strict

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

end;

thus cherry is strict ; :: thesis: verum