let Z be finite Tree; :: thesis: ( branchdeg (Root Z) = 0 implies ( card Z = 1 & Z = {{}} ) )
assume branchdeg (Root Z) = 0 ; :: thesis: ( card Z = 1 & Z = {{}} )
then 0 = card (succ (Root Z)) by TREES_2:def 12;
then A1: succ (Root Z) = {} ;

now :: thesis: for x being object holds
( ( x in Z implies x in {(Root Z)} ) & ( x in {(Root Z)} implies x in Z ) )

let x be object ; :: thesis: ( ( x in Z implies x in {(Root Z)} ) & ( x in {(Root Z)} implies x in Z ) )
thus ( x in Z implies x in {(Root Z)} ) :: thesis: ( x in {(Root Z)} implies x in Z )

proof

assume x in Z ; :: thesis: x in {(Root Z)}
then reconsider z = x as Element of Z ;
assume not x in {(Root Z)} ; :: thesis: contradiction
then z <> Root Z by TARSKI:def 1;
then consider w being FinSequence of NAT , n being Element of NAT such that
A2: z = <*n*> ^ w by FINSEQ_2:130;
<*n*> is_a_prefix_of z by A2, TREES_1:1;
then <*n*> in Z by TREES_1:20;
then {} ^ <*n*> in Z by FINSEQ_1:34;
hence contradiction by A1, TREES_2:12; :: thesis: verum

end;

assume x in {(Root Z)} ; :: thesis: x in Z
then reconsider x9 = x as Element of Z ;
x9 in Z ;
hence x in Z ; :: thesis: verum

end;

then Z = {(Root Z)} by TARSKI:2;
hence ( card Z = 1 & Z = {{}} ) by CARD_2:42; :: thesis: verum