let T be Tree; :: thesis: ( T = {0,1} * iff for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} )
thus ( T = {0,1} * implies for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) :: thesis: ( ( for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) implies T = {0,1} * )

proof

assume A1: T = {0,1} * ; :: thesis: for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)}
let t be Element of T; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}
( T is binary & not t in Leaves T ) by A1, Th3, Th4;
hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by BINTREE1:def 2; :: thesis: verum

end;

assume A2: for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ; :: thesis: T = {0,1} *
thus T = {0,1} * :: thesis: verum

proof

thus T c= {0,1} * :: according to XBOOLE_0:def 10 :: thesis: {0,1} * c= T

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in T or x in {0,1} * )
assume A3: x in T ; :: thesis: x in {0,1} *
T is binary by A2, Th7;
then x is FinSequence of {0,1} by A3, Th2;
hence x in {0,1} * by FINSEQ_1:def 11; :: thesis: verum

end;

defpred S₁[ FinSequence] means $1 in T;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {0,1} * or x in T )
assume x in {0,1} * ; :: thesis: x in T
then A4: x is FinSequence of {0,1} by FINSEQ_1:def 11;
A5: for p being FinSequence of {0,1}
for n being Element of {0,1} st S₁[p] holds
S₁[p ^ <*n*>]

proof

let p be FinSequence of {0,1}; :: thesis: for n being Element of {0,1} st S₁[p] holds
S₁[p ^ <*n*>]
let n be Element of {0,1}; :: thesis: ( S₁[p] implies S₁[p ^ <*n*>] )
A6: ( n = 0 or n = 1 ) by TARSKI:def 2;
assume p in T ; :: thesis: S₁[p ^ <*n*>]
then reconsider p1 = p as Element of T ;
succ p1 = {(p1 ^ <*0*>),(p1 ^ <*1*>)} by A2;
then p ^ <*n*> in succ p1 by A6, TARSKI:def 2;
hence S₁[p ^ <*n*>] ; :: thesis: verum

end;

A7: S₁[ <*> {0,1}] by TREES_1:22;
for p being FinSequence of {0,1} holds S₁[p] from FINSEQ_2:sch 2(A7, A5);
hence x in T by A4; :: thesis: verum

end;