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 A1: ( T1 is binary & 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 A2: 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
A3: ( ( p in T1 & t = <*0 *> ^ p ) or ( p in T2 & t = <*1*> ^ p ) ) ;

A4: now

assume A5: ( p in T1 & t = <*0 *> ^ p ) ; :: thesis: succ t = {(t ^ <*0 *>),(t ^ <*1*>)}
then reconsider p = p as Element of T1 ;

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 A2, A5, Th8; :: thesis: verum

end;

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

then A6: 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 A7: 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
A8: ( x = t ^ <*n*> & t ^ <*n*> in tree T1,T2 ) ;
A9: x = <*0 *> ^ (p ^ <*n*>) by A5, A8, FINSEQ_1:45;
then reconsider pn = p ^ <*n*> as Element of T1 by A8, TREES_3:72;
pn in succ p by A5, A7, A9, Th9;
then ( pn = p ^ <*0 *> or pn = p ^ <*1*> ) by A6, TARSKI:def 2;
then ( x = t ^ <*0 *> or x = t ^ <*1*> ) by A8, 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 A5, TARSKI:def 2;
then A10: ( x = <*0 *> ^ (p ^ <*0 *>) or x = <*0 *> ^ (p ^ <*1*>) ) by FINSEQ_1:45;
( p ^ <*0 *> in succ p & p ^ <*1*> in succ p ) by A6, TARSKI:def 2;
hence x in succ t by A5, A10, Th9; :: thesis: verum

end;

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

end;

end;

end;

now

assume A11: ( p in T2 & t = <*1*> ^ p ) ; :: thesis: succ t = {(t ^ <*0 *>),(t ^ <*1*>)}
then reconsider p = p as Element of T2 ;

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 A2, A11, Th8; :: thesis: verum

end;

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

then A12: 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 A13: 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
A14: ( x = t ^ <*n*> & t ^ <*n*> in tree T1,T2 ) ;
A15: x = <*1*> ^ (p ^ <*n*>) by A11, A14, FINSEQ_1:45;
then reconsider pn = p ^ <*n*> as Element of T2 by A14, TREES_3:73;
pn in succ p by A11, A13, A15, Th9;
then ( pn = p ^ <*0 *> or pn = p ^ <*1*> ) by A12, TARSKI:def 2;
then ( x = t ^ <*0 *> or x = t ^ <*1*> ) by A14, 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 A11, TARSKI:def 2;
then A16: ( x = <*1*> ^ (p ^ <*0 *>) or x = <*1*> ^ (p ^ <*1*>) ) by FINSEQ_1:45;
( p ^ <*0 *> in succ p & p ^ <*1*> in succ p ) by A12, TARSKI:def 2;
hence x in succ t by A11, A16, 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 A3, A4; :: thesis: verum

end;

end;

end;

hence tree T1,T2 is binary by Def2; :: thesis: verum

end;

assume A17: 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 A18: succ zt = {((<*0 *> ^ t) ^ <*0 *>),((<*0 *> ^ t) ^ <*1*>)} by A17, Def2;
A19: 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
A20: ( x = t ^ <*n*> & t ^ <*n*> in T1 ) ;
<*0 *> ^ (t ^ <*n*>) in tree T1,T2 by A20, 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 A18, A19, TARSKI:def 2;
then ( x = t ^ <*0 *> or x = t ^ <*1*> ) by A20, 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 A21: ( x = t ^ <*0 *> or x = t ^ <*1*> ) by TARSKI:def 2;
( (<*0 *> ^ t) ^ <*0 *> in succ zt & (<*0 *> ^ t) ^ <*1*> in succ zt ) by A18, TARSKI:def 2;
then ( <*0 *> ^ (t ^ <*0 *>) in succ zt & <*0 *> ^ (t ^ <*1*>) in succ zt ) by FINSEQ_1:45;
hence x in succ t by A21, 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 A22: succ zt = {((<*1*> ^ t) ^ <*0 *>),((<*1*> ^ t) ^ <*1*>)} by A17, Def2;
A23: 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
A24: ( x = t ^ <*n*> & t ^ <*n*> in T2 ) ;
<*1*> ^ (t ^ <*n*>) in tree T1,T2 by A24, 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 A22, A23, TARSKI:def 2;
then ( x = t ^ <*0 *> or x = t ^ <*1*> ) by A24, 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 A25: ( x = t ^ <*0 *> or x = t ^ <*1*> ) by TARSKI:def 2;
( (<*1*> ^ t) ^ <*0 *> in succ zt & (<*1*> ^ t) ^ <*1*> in succ zt ) by A22, TARSKI:def 2;
then ( <*1*> ^ (t ^ <*0 *>) in succ zt & <*1*> ^ (t ^ <*1*>) in succ zt ) by FINSEQ_1:45;
hence x in succ t by A25, 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