let T be Tree; :: thesis: ( T = {0 ,1} * implies T is binary )
assume A1: T = {0 ,1} * ; :: thesis: T is binary

now

let t be Element of T; :: thesis: ( not t in Leaves T implies succ t = {(t ^ <*0 *>),(t ^ <*1*>)} )
assume not t in Leaves T ; :: thesis: succ t = {(t ^ <*0 *>),(t ^ <*1*>)}
{ (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T } = {(t ^ <*0 *>),(t ^ <*1*>)}

proof

thus { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T } c= {(t ^ <*0 *>),(t ^ <*1*>)} :: according to XBOOLE_0:def 10 :: thesis: {(t ^ <*0 *>),(t ^ <*1*>)} c= { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T } or x in {(t ^ <*0 *>),(t ^ <*1*>)} )
assume x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T } ; :: thesis: x in {(t ^ <*0 *>),(t ^ <*1*>)}
then consider n being Element of NAT such that
A2: x = t ^ <*n*> and
A3: t ^ <*n*> in T ;
reconsider tn = t ^ <*n*> as FinSequence of {0 ,1} by A1, A3, FINSEQ_1:def 11;
(len t) + 1 in Seg ((len t) + 1) by FINSEQ_1:6;
then (len t) + 1 in Seg (len tn) by FINSEQ_2:19;
then (len t) + 1 in dom tn by FINSEQ_1:def 3;
then tn /. ((len t) + 1) = (t ^ <*n*>) . ((len t) + 1) by PARTFUN1:def 8
.= n by FINSEQ_1:59 ;
then ( n = 0 or n = 1 ) by TARSKI:def 2;
hence x in {(t ^ <*0 *>),(t ^ <*1*>)} by A2, TARSKI:def 2; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(t ^ <*0 *>),(t ^ <*1*>)} or x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T } )
A4: t is FinSequence of {0 ,1} by A1, FINSEQ_1:def 11;
rng <*0 *> c= {0 ,1}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng <*0 *> or z in {0 ,1} )
assume z in rng <*0 *> ; :: thesis: z in {0 ,1}
then z in {0 } by FINSEQ_1:55;
then z = 0 by TARSKI:def 1;
hence z in {0 ,1} by TARSKI:def 2; :: thesis: verum

end;

then A5: <*0 *> is FinSequence of {0 ,1} by FINSEQ_1:def 4;
rng <*1*> c= {0 ,1}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng <*1*> or z in {0 ,1} )
assume z in rng <*1*> ; :: thesis: z in {0 ,1}
then z in {1} by FINSEQ_1:55;
then z = 1 by TARSKI:def 1;
hence z in {0 ,1} by TARSKI:def 2; :: thesis: verum

end;

then A6: <*1*> is FinSequence of {0 ,1} by FINSEQ_1:def 4;
t ^ <*0 *> is FinSequence of {0 ,1} by A4, A5, Lm1;
then A7: t ^ <*0 *> in T by A1, FINSEQ_1:def 11;
t ^ <*1*> is FinSequence of {0 ,1} by A4, A6, Lm1;
then A8: t ^ <*1*> in T by A1, FINSEQ_1:def 11;
assume x in {(t ^ <*0 *>),(t ^ <*1*>)} ; :: thesis: x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T }
then ( x = t ^ <*0 *> or x = t ^ <*1*> ) by TARSKI:def 2;
hence x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T } by A7, A8; :: thesis: verum

end;

hence succ t = {(t ^ <*0 *>),(t ^ <*1*>)} by TREES_2:def 5; :: thesis: verum

end;

hence T is binary by BINTREE1:def 2; :: thesis: verum