let T1, T2 be Tree; :: thesis: ( ( T1 is binary & T2 is binary ) iff tree (T1,T2) is binary )
set RT = tree (T1,T2);

hereby :: thesis: ( tree (T1,T2) is binary implies ( T1 is binary & T2 is binary ) )

assume that
A1: T1 is binary and
A2: T2 is binary ; :: thesis: tree (T1,T2) is binary

now :: thesis: for t being Element of tree (T1,T2) st not t in Leaves (tree (T1,T2)) holds
succ t = {(t ^ <*0*>),(t ^ <*1*>)}

let t be Element of tree (T1,T2); :: thesis: ( not t in Leaves (tree (T1,T2)) implies succ b₁ = {(b₁ ^ <*0*>),(b₁ ^ <*1*>)} )
assume A3: not t in Leaves (tree (T1,T2)) ; :: thesis: succ b₁ = {(b₁ ^ <*0*>),(b₁ ^ <*1*>)}

per cases ( t = {} or ex p being FinSequence st
( ( p in T1 & t = <*0*> ^ p ) or ( p in T2 & t = <*1*> ^ p ) ) ) by TREES_3:68;

suppose t = {} ; :: thesis: succ b₁ = {(b₁ ^ <*0*>),(b₁ ^ <*1*>)}

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

end;

suppose ex p being FinSequence st
( ( p in T1 & t = <*0*> ^ p ) or ( p in T2 & t = <*1*> ^ p ) ) ; :: thesis: succ b₁ = {(b₁ ^ <*0*>),(b₁ ^ <*1*>)}

then consider p being FinSequence such that
A4: ( ( p in T1 & t = <*0*> ^ p ) or ( p in T2 & t = <*1*> ^ p ) ) ;

A5: now :: thesis: ( p in T2 & t = <*1*> ^ p implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} )

assume that
A6: p in T2 and
A7: t = <*1*> ^ p ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}
reconsider p = p as Element of T2 by A6;

per cases ( p in Leaves T2 or not p in Leaves T2 ) ;

suppose p in Leaves T2 ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}

hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A3, A7, Th6; :: thesis: verum

end;

suppose not p in Leaves T2 ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}

then A8: succ p = {(p ^ <*0*>),(p ^ <*1*>)} by A2;

now :: thesis: for x being object holds
( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) )

let x be object ; :: thesis: ( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) )

hereby :: thesis: ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t )

assume A9: x in succ t ; :: thesis: x in {(t ^ <*0*>),(t ^ <*1*>)}
then x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in tree (T1,T2) } by TREES_2:def 5;
then consider n being Nat such that
A10: x = t ^ <*n*> and
A11: t ^ <*n*> in tree (T1,T2) ;
A12: x = <*1*> ^ (p ^ <*n*>) by A7, A10, FINSEQ_1:32;
then reconsider pn = p ^ <*n*> as Element of T2 by A10, A11, TREES_3:70;
pn in succ p by A7, A9, A12, Th7;
then ( pn = p ^ <*0*> or pn = p ^ <*1*> ) by A8, TARSKI:def 2;
then ( x = t ^ <*0*> or x = t ^ <*1*> ) by A10, FINSEQ_1:33;
hence x in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum

end;

assume x in {(t ^ <*0*>),(t ^ <*1*>)} ; :: thesis: x in succ t
then ( x = (<*1*> ^ p) ^ <*0*> or x = (<*1*> ^ p) ^ <*1*> ) by A7, TARSKI:def 2;
then A13: ( x = <*1*> ^ (p ^ <*0*>) or x = <*1*> ^ (p ^ <*1*>) ) by FINSEQ_1:32;
( p ^ <*0*> in succ p & p ^ <*1*> in succ p ) by A8, TARSKI:def 2;
hence x in succ t by A7, A13, Th7; :: thesis: verum

end;

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

end;

end;

end;

now :: thesis: ( p in T1 & t = <*0*> ^ p implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} )

assume that
A14: p in T1 and
A15: t = <*0*> ^ p ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}
reconsider p = p as Element of T1 by A14;

per cases ( p in Leaves T1 or not p in Leaves T1 ) ;

suppose p in Leaves T1 ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}

hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A3, A15, Th6; :: thesis: verum

end;

suppose not p in Leaves T1 ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}

then A16: succ p = {(p ^ <*0*>),(p ^ <*1*>)} by A1;

now :: thesis: for x being object holds
( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) )

let x be object ; :: thesis: ( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) )

hereby :: thesis: ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t )

assume A17: x in succ t ; :: thesis: x in {(t ^ <*0*>),(t ^ <*1*>)}
then x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in tree (T1,T2) } by TREES_2:def 5;
then consider n being Nat such that
A18: x = t ^ <*n*> and
A19: t ^ <*n*> in tree (T1,T2) ;
A20: x = <*0*> ^ (p ^ <*n*>) by A15, A18, FINSEQ_1:32;
then reconsider pn = p ^ <*n*> as Element of T1 by A18, A19, TREES_3:69;
pn in succ p by A15, A17, A20, Th7;
then ( pn = p ^ <*0*> or pn = p ^ <*1*> ) by A16, TARSKI:def 2;
then ( x = t ^ <*0*> or x = t ^ <*1*> ) by A18, FINSEQ_1:33;
hence x in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum

end;

assume x in {(t ^ <*0*>),(t ^ <*1*>)} ; :: thesis: x in succ t
then ( x = (<*0*> ^ p) ^ <*0*> or x = (<*0*> ^ p) ^ <*1*> ) by A15, TARSKI:def 2;
then A21: ( x = <*0*> ^ (p ^ <*0*>) or x = <*0*> ^ (p ^ <*1*>) ) by FINSEQ_1:32;
( p ^ <*0*> in succ p & p ^ <*1*> in succ p ) by A16, TARSKI:def 2;
hence x in succ t by A15, A21, Th7; :: thesis: verum

end;

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

end;

end;

end;

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

end;

end;

end;

hence tree (T1,T2) is binary ; :: thesis: verum

end;

assume A22: tree (T1,T2) is binary ; :: thesis: ( T1 is binary & T2 is binary )

now :: thesis: for t being Element of T1 st not t in Leaves T1 holds
succ t = {(t ^ <*0*>),(t ^ <*1*>)}

let t be Element of T1; :: thesis: ( not t in Leaves T1 implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} )
reconsider zt = <*0*> ^ t as Element of tree (T1,T2) by TREES_3:69;
assume not t in Leaves T1 ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}
then not zt in Leaves (tree (T1,T2)) by Th6;
then A23: succ zt = {((<*0*> ^ t) ^ <*0*>),((<*0*> ^ t) ^ <*1*>)} by A22;
A24: succ zt = { (zt ^ <*n*>) where n is Nat : zt ^ <*n*> in tree (T1,T2) } by TREES_2:def 5;

now :: thesis: for x being object holds
( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) )

let x be object ; :: thesis: ( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) )

hereby :: thesis: ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t )

assume x in succ t ; :: thesis: x in {(t ^ <*0*>),(t ^ <*1*>)}
then x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in T1 } by TREES_2:def 5;
then consider n being Nat such that
A25: x = t ^ <*n*> and
A26: t ^ <*n*> in T1 ;
<*0*> ^ (t ^ <*n*>) in tree (T1,T2) by A26, TREES_3:69;
then zt ^ <*n*> in tree (T1,T2) by FINSEQ_1:32;
then zt ^ <*n*> in { (zt ^ <*k*>) where k is Nat : zt ^ <*k*> in tree (T1,T2) } ;
then ( zt ^ <*n*> = zt ^ <*0*> or zt ^ <*n*> = zt ^ <*1*> ) by A23, A24, TARSKI:def 2;
then ( x = t ^ <*0*> or x = t ^ <*1*> ) by A25, FINSEQ_1:33;
hence x in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum

end;

assume x in {(t ^ <*0*>),(t ^ <*1*>)} ; :: thesis: x in succ t
then A27: ( x = t ^ <*0*> or x = t ^ <*1*> ) by TARSKI:def 2;
(<*0*> ^ t) ^ <*1*> in succ zt by A23, TARSKI:def 2;
then A28: <*0*> ^ (t ^ <*1*>) in succ zt by FINSEQ_1:32;
(<*0*> ^ t) ^ <*0*> in succ zt by A23, TARSKI:def 2;
then <*0*> ^ (t ^ <*0*>) in succ zt by FINSEQ_1:32;
hence x in succ t by A27, A28, Th7; :: thesis: verum

end;

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

end;

hence T1 is binary ; :: thesis: T2 is binary

now :: thesis: for t being Element of T2 st not t in Leaves T2 holds
succ t = {(t ^ <*0*>),(t ^ <*1*>)}

let t be Element of T2; :: thesis: ( not t in Leaves T2 implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} )
reconsider zt = <*1*> ^ t as Element of tree (T1,T2) by TREES_3:70;
assume not t in Leaves T2 ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}
then not zt in Leaves (tree (T1,T2)) by Th6;
then A29: succ zt = {((<*1*> ^ t) ^ <*0*>),((<*1*> ^ t) ^ <*1*>)} by A22;
A30: succ zt = { (zt ^ <*n*>) where n is Nat : zt ^ <*n*> in tree (T1,T2) } by TREES_2:def 5;

now :: thesis: for x being object holds
( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) )

let x be object ; :: thesis: ( ( x in succ t implies x in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t ) )

hereby :: thesis: ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in succ t )

assume x in succ t ; :: thesis: x in {(t ^ <*0*>),(t ^ <*1*>)}
then x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in T2 } by TREES_2:def 5;
then consider n being Nat such that
A31: x = t ^ <*n*> and
A32: t ^ <*n*> in T2 ;
<*1*> ^ (t ^ <*n*>) in tree (T1,T2) by A32, TREES_3:70;
then zt ^ <*n*> in tree (T1,T2) by FINSEQ_1:32;
then zt ^ <*n*> in { (zt ^ <*k*>) where k is Nat : zt ^ <*k*> in tree (T1,T2) } ;
then ( zt ^ <*n*> = zt ^ <*0*> or zt ^ <*n*> = zt ^ <*1*> ) by A29, A30, TARSKI:def 2;
then ( x = t ^ <*0*> or x = t ^ <*1*> ) by A31, FINSEQ_1:33;
hence x in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum

end;

assume x in {(t ^ <*0*>),(t ^ <*1*>)} ; :: thesis: x in succ t
then A33: ( x = t ^ <*0*> or x = t ^ <*1*> ) by TARSKI:def 2;
(<*1*> ^ t) ^ <*1*> in succ zt by A29, TARSKI:def 2;
then A34: <*1*> ^ (t ^ <*1*>) in succ zt by FINSEQ_1:32;
(<*1*> ^ t) ^ <*0*> in succ zt by A29, TARSKI:def 2;
then <*1*> ^ (t ^ <*0*>) in succ zt by FINSEQ_1:32;
hence x in succ t by A33, A34, Th7; :: thesis: verum

end;

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

end;

hence T2 is binary ; :: thesis: verum