let Z be finite Tree; :: thesis: ( branchdeg (Root Z) = 2 implies succ (Root Z) = {<*0*>,<*1*>} )
assume branchdeg (Root Z) = 2 ; :: thesis: 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 ; :: thesis: succ (Root Z) = {<*0*>,<*1*>}

now :: thesis: not k <> 1

A10: <*1*> = (Root Z) ^ <*1*> by FINSEQ_1:34;
assume A11: k <> 1 ; :: thesis: contradiction
then 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; :: thesis: verum

end;

hence succ (Root Z) = {<*0*>,<*1*>} by A2, A4, A8, A9, FINSEQ_1:34; :: thesis: verum

end;

suppose A12: m <> 0 ; :: thesis: 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 :: thesis: not m <> 1

A14: <*1*> = (Root Z) ^ <*1*> by FINSEQ_1:34;
assume A15: m <> 1 ; :: thesis: contradiction
then 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; :: thesis: verum

end;

hence succ (Root Z) = {<*0*>,<*1*>} by A2, A4, A8, A13, FINSEQ_1:34, TREES_1:3; :: thesis: verum

end;

end;