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 13;
then consider x, y being set such that
A1: ( x <> y & succ (Root Z) = {x,y} ) by CARD_2:79;
A2: ( x in succ (Root Z) & y in succ (Root Z) ) by A1, TARSKI:def 2;
then reconsider x' = x as Element of Z ;
reconsider y' = y as Element of Z by A2;
x' in { ((Root Z) ^ <*n*>) where n is Element of NAT : (Root Z) ^ <*n*> in Z } by A2, TREES_2:def 5;
then consider m being Element of NAT such that
A3: ( x' = (Root Z) ^ <*m*> & (Root Z) ^ <*m*> in Z ) ;
A4: x' = <*m*> by A3, FINSEQ_1:47;
y' in { ((Root Z) ^ <*n*>) where n is Element of NAT : (Root Z) ^ <*n*> in Z } by A2, TREES_2:def 5;
then consider k being Element of NAT such that
A5: ( y' = (Root Z) ^ <*k*> & (Root Z) ^ <*k*> in Z ) ;
A6: y' = <*k*> by A5, FINSEQ_1:47;

per cases ( m = 0 or m <> 0 ) ;

suppose A7: m = 0 ; :: thesis: succ (Root Z) = {<*0 *>,<*1*>}

now

assume A8: k <> 1 ; :: thesis: contradiction
then 2 <= k by A1, A4, A6, A7, NAT_1:27;
then A9: <*1*> in Z by A6, Th11, XXREAL_0:2;
<*1*> = (Root Z) ^ <*1*> by FINSEQ_1:47;
then <*1*> in succ (Root Z) by A9, TREES_2:14;
then ( <*1*> = <*0 *> or <*1*> = <*k*> ) by A1, A4, A6, A7, TARSKI:def 2;
hence contradiction by A8, TREES_1:16; :: thesis: verum

end;

hence succ (Root Z) = {<*0 *>,<*1*>} by A1, A3, A6, A7, FINSEQ_1:47; :: thesis: verum

end;

suppose A10: m <> 0 ; :: thesis: succ (Root Z) = {<*0 *>,<*1*>}

A11: <*0 *> in Z by A4, Th11, NAT_1:2;
<*0 *> = (Root Z) ^ <*0 *> by FINSEQ_1:47;
then <*0 *> in succ (Root Z) by A11, TREES_2:14;
then A12: ( <*0 *> = <*m*> or <*0 *> = <*k*> ) by A1, A4, A6, TARSKI:def 2;

now

assume A13: m <> 1 ; :: thesis: contradiction
then 2 <= m by A10, NAT_1:27;
then A14: <*1*> in Z by A4, Th11, XXREAL_0:2;
<*1*> = (Root Z) ^ <*1*> by FINSEQ_1:47;
then <*1*> in succ (Root Z) by A14, TREES_2:14;
then ( <*1*> = <*0 *> or <*1*> = <*m*> ) by A1, A4, A6, A10, A12, TARSKI:def 2, TREES_1:16;
hence contradiction by A13, TREES_1:16; :: thesis: verum

end;

hence succ (Root Z) = {<*0 *>,<*1*>} by A1, A3, A6, A12, FINSEQ_1:47, TREES_1:16; :: thesis: verum

end;

end;