let Z be finite Tree; ( branchdeg (Root Z) = 2 implies succ (Root Z) = {<*0*>,<*1*>} )
assume
branchdeg (Root Z) = 2
; succ (Root Z) = {<*0*>,<*1*>}
then
card (succ (Root Z)) = 2
by TREES_2:def 12;
then consider x, y being object such that
A1:
x <> y
and
A2:
succ (Root Z) = {x,y}
by CARD_2:60;
A3:
x in succ (Root Z)
by A2, TARSKI:def 2;
then reconsider x9 = x as Element of Z ;
x9 in { ((Root Z) ^ <*n*>) where n is Nat : (Root Z) ^ <*n*> in Z }
by A3, TREES_2:def 5;
then consider m being Nat such that
A4:
x9 = (Root Z) ^ <*m*>
and
(Root Z) ^ <*m*> in Z
;
A5:
x9 = <*m*>
by A4, FINSEQ_1:34;
A6:
y in succ (Root Z)
by A2, TARSKI:def 2;
then reconsider y9 = y as Element of Z ;
y9 in { ((Root Z) ^ <*n*>) where n is Nat : (Root Z) ^ <*n*> in Z }
by A6, TREES_2:def 5;
then consider k being Nat such that
A7:
y9 = (Root Z) ^ <*k*>
and
(Root Z) ^ <*k*> in Z
;
A8:
y9 = <*k*>
by A7, FINSEQ_1:34;
per cases
( m = 0 or m <> 0 )
;
suppose A9:
m = 0
;
succ (Root Z) = {<*0*>,<*1*>}now not k <> 1A10:
<*1*> = (Root Z) ^ <*1*>
by FINSEQ_1:34;
assume A11:
k <> 1
;
contradictionthen
k <> 0 & ... &
k <> 1
by A1, A5, A8, A9;
then
1
< k
by NAT_1:25;
then
1
+ 1
<= k
by NAT_1:13;
then
<*1*> in Z
by A8, Th3, XXREAL_0:2;
then
<*1*> in succ (Root Z)
by A10, TREES_2:12;
then
(
<*1*> = <*0*> or
<*1*> = <*k*> )
by A2, A5, A8, A9, TARSKI:def 2;
hence
contradiction
by A11, TREES_1:3;
verum end; hence
succ (Root Z) = {<*0*>,<*1*>}
by A2, A4, A8, A9, FINSEQ_1:34;
verum suppose A12:
m <> 0
;
succ (Root Z) = {<*0*>,<*1*>}
(
<*0*> in Z &
<*0*> = (Root Z) ^ <*0*> )
by A5, Th3, FINSEQ_1:34, NAT_1:2;
then
<*0*> in succ (Root Z)
by TREES_2:12;
then A13:
(
<*0*> = <*m*> or
<*0*> = <*k*> )
by A2, A5, A8, TARSKI:def 2;
now not m <> 1A14:
<*1*> = (Root Z) ^ <*1*>
by FINSEQ_1:34;
assume A15:
m <> 1
;
contradictionthen
1
< m
by A12, NAT_1:25;
then
1
+ 1
<= m
by NAT_1:13;
then
<*1*> in Z
by A5, Th3, XXREAL_0:2;
then
<*1*> in succ (Root Z)
by A14, TREES_2:12;
then
(
<*1*> = <*0*> or
<*1*> = <*m*> )
by A2, A5, A8, A12, A13, TARSKI:def 2, TREES_1:3;
hence
contradiction
by A15, TREES_1:3;
verum end; hence
succ (Root Z) = {<*0*>,<*1*>}
by A2, A4, A8, A13, FINSEQ_1:34, TREES_1:3;
verum