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

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:71;

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

hence succ t = {(t ^ <*0 *>),(t ^ <*1*>)} by Th9; :: 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

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, Th8; :: 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, Def2;

now

let x be set ; :: 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 Element of NAT : t ^ <*n*> in tree T1,T2 } by TREES_2:def 5;
then consider n being Element of 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:45;
then reconsider pn = p ^ <*n*> as Element of T2 by A10, A11, TREES_3:73;
pn in succ p by A7, A9, A12, Th9;
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:46;
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:45;
( p ^ <*0 *> in succ p & p ^ <*1*> in succ p ) by A8, TARSKI:def 2;
hence x in succ t by A7, A13, Th9; :: thesis: verum

end;

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

end;

end;

end;

now

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, Th8; :: 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, Def2;

now

let x be set ; :: 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 Element of NAT : t ^ <*n*> in tree T1,T2 } by TREES_2:def 5;
then consider n being Element of 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:45;
then reconsider pn = p ^ <*n*> as Element of T1 by A18, A19, TREES_3:72;
pn in succ p by A15, A17, A20, Th9;
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:46;
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:45;
( p ^ <*0 *> in succ p & p ^ <*1*> in succ p ) by A16, TARSKI:def 2;
hence x in succ t by A15, A21, Th9; :: 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 by Def2; :: thesis: verum

end;

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

now

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:72;
assume not t in Leaves T1 ; :: thesis: succ t = {(t ^ <*0 *>),(t ^ <*1*>)}
then not zt in Leaves (tree T1,T2) by Th8;
then A23: succ zt = {((<*0 *> ^ t) ^ <*0 *>),((<*0 *> ^ t) ^ <*1*>)} by A22, Def2;
A24: succ zt = { (zt ^ <*n*>) where n is Element of NAT : zt ^ <*n*> in tree T1,T2 } by TREES_2:def 5;

now

let x be set ; :: 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 Element of NAT : t ^ <*n*> in T1 } by TREES_2:def 5;
then consider n being Element of NAT such that
A25: x = t ^ <*n*> and
A26: t ^ <*n*> in T1 ;
<*0 *> ^ (t ^ <*n*>) in tree T1,T2 by A26, TREES_3:72;
then zt ^ <*n*> in tree T1,T2 by FINSEQ_1:45;
then zt ^ <*n*> in { (zt ^ <*k*>) where k is Element of 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:46;
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:45;
(<*0 *> ^ t) ^ <*0 *> in succ zt by A23, TARSKI:def 2;
then <*0 *> ^ (t ^ <*0 *>) in succ zt by FINSEQ_1:45;
hence x in succ t by A27, A28, Th9; :: thesis: verum

end;

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

end;

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

now

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:73;
assume not t in Leaves T2 ; :: thesis: succ t = {(t ^ <*0 *>),(t ^ <*1*>)}
then not zt in Leaves (tree T1,T2) by Th8;
then A29: succ zt = {((<*1*> ^ t) ^ <*0 *>),((<*1*> ^ t) ^ <*1*>)} by A22, Def2;
A30: succ zt = { (zt ^ <*n*>) where n is Element of NAT : zt ^ <*n*> in tree T1,T2 } by TREES_2:def 5;

now

let x be set ; :: 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 Element of NAT : t ^ <*n*> in T2 } by TREES_2:def 5;
then consider n being Element of NAT such that
A31: x = t ^ <*n*> and
A32: t ^ <*n*> in T2 ;
<*1*> ^ (t ^ <*n*>) in tree T1,T2 by A32, TREES_3:73;
then zt ^ <*n*> in tree T1,T2 by FINSEQ_1:45;
then zt ^ <*n*> in { (zt ^ <*k*>) where k is Element of 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:46;
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:45;
(<*1*> ^ t) ^ <*0 *> in succ zt by A29, TARSKI:def 2;
then <*1*> ^ (t ^ <*0 *>) in succ zt by FINSEQ_1:45;
hence x in succ t by A33, A34, Th9; :: thesis: verum

end;

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

end;

hence T2 is binary by Def2; :: thesis: verum