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 S1[ 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 S1[p] holds
S1[p ^ <*n*>]
proof
let p be FinSequence of {0,1}; :: thesis: for n being Element of {0,1} st S1[p] holds
S1[p ^ <*n*>]
let n be Element of {0,1}; :: thesis: ( S1[p] implies S1[p ^ <*n*>] )
A6: ( n = 0 or n = 1 ) by TARSKI:def 2;
assume p in T ; :: thesis: S1[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 S1[p ^ <*n*>] ; :: thesis: verum
end;
A7: S1[ <*> {0,1}] by TREES_1:22;
for p being FinSequence of {0,1} holds S1[p] from FINSEQ_2:sch 2(A7, A5);
 hence x in T by A4; :: thesis: verum
end;