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} * )

thus T = {0,1} * :: thesis: verum

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 A2:
for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)}
; :: thesis: T = {0,1} *
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;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

thus T = {0,1} * :: thesis: verum

proof

thus
T c= {0,1} *
:: according to XBOOLE_0:def 10 :: thesis: {0,1} * c= T_{1}[ 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_{1}[p] holds

S_{1}[p ^ <*n*>]
_{1}[ <*> {0,1}]
by TREES_1:22;

for p being FinSequence of {0,1} holds S_{1}[p]
from FINSEQ_2:sch 2(A7, A5);

hence x in T by A4; :: thesis: verum

end;proof

defpred S
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;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

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

S

proof

A7:
S
let p be FinSequence of {0,1}; :: thesis: for n being Element of {0,1} st S_{1}[p] holds

S_{1}[p ^ <*n*>]

let n be Element of {0,1}; :: thesis: ( S_{1}[p] implies S_{1}[p ^ <*n*>] )

A6: ( n = 0 or n = 1 ) by TARSKI:def 2;

assume p in T ; :: thesis: S_{1}[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_{1}[p ^ <*n*>]
; :: thesis: verum

end;S

let n be Element of {0,1}; :: thesis: ( S

A6: ( n = 0 or n = 1 ) by TARSKI:def 2;

assume p in T ; :: thesis: S

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

for p being FinSequence of {0,1} holds S

hence x in T by A4; :: thesis: verum