set e = elementary_tree 1;
A1: <*0 *> in elementary_tree 1 by TARSKI:def 2, TREES_1:88;
let Z be finite Tree; :: thesis: for z being Element of Z st succ (Root Z) = {z} holds
Z = (elementary_tree 1) with-replacement <*0 *>,(Z | z)
let z be Element of Z; :: thesis: ( succ (Root Z) = {z} implies Z = (elementary_tree 1) with-replacement <*0 *>,(Z | z) )
assume A2: succ (Root Z) = {z} ; :: thesis: Z = (elementary_tree 1) with-replacement <*0 *>,(Z | z)
then card (succ (Root Z)) = 1 by CARD_1:50;
then branchdeg (Root Z) = 1 by TREES_2:def 13;
then {z} = {<*0 *>} by A2, Th23;
then z in {<*0 *>} by TARSKI:def 1;
then A3: z = <*0 *> by TARSKI:def 1;
then A4: <*0 *> in Z ;
A5: {} in Z by TREES_1:47;

now

let x be set ; :: thesis: ( ( x in Z implies x in (elementary_tree 1) with-replacement <*0 *>,(Z | z) ) & ( x in (elementary_tree 1) with-replacement <*0 *>,(Z | z) implies b₁ in Z ) )
thus ( x in Z implies x in (elementary_tree 1) with-replacement <*0 *>,(Z | z) ) :: thesis: ( x in (elementary_tree 1) with-replacement <*0 *>,(Z | z) implies b₁ in Z )

proof

assume x in Z ; :: thesis: x in (elementary_tree 1) with-replacement <*0 *>,(Z | z)
then reconsider x' = x as Element of Z ;

per cases ( x' = {} or x' <> {} ) ;

suppose x' = {} ; :: thesis: x in (elementary_tree 1) with-replacement <*0 *>,(Z | z)

hence x in (elementary_tree 1) with-replacement <*0 *>,(Z | z) by TREES_1:47; :: thesis: verum

end;

suppose x' <> {} ; :: thesis: x in (elementary_tree 1) with-replacement <*0 *>,(Z | z)

then consider w being FinSequence of NAT , n being Nat such that
A6: x' = <*n*> ^ w by FINSEQ_2:150;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
<*n*> is_a_prefix_of x' by A6, TREES_1:8;
then A7: <*n*> in Z by TREES_1:45;
<*n*> = (Root Z) ^ <*n*> by FINSEQ_1:47;
then A8: <*n*> in succ (Root Z) by A7, TREES_2:14;
then A9: <*n*> = <*0 *> by A2, A3, TARSKI:def 1;
<*n*> = z by A2, A8, TARSKI:def 1;
then w in Z | z by A6, TREES_1:def 9;
hence x in (elementary_tree 1) with-replacement <*0 *>,(Z | z) by A1, A6, A9, TREES_1:def 12; :: thesis: verum

end;

end;

end;

assume x in (elementary_tree 1) with-replacement <*0 *>,(Z | z) ; :: thesis: b₁ in Z
then reconsider x' = x as Element of (elementary_tree 1) with-replacement <*0 *>,(Z | z) ;

per cases ( ( x' in elementary_tree 1 & not <*0 *> is_a_proper_prefix_of x' ) or ex s being FinSequence of NAT st
( s in Z | z & x' = <*0 *> ^ s ) ) by A1, TREES_1:def 12;

suppose ( x' in elementary_tree 1 & not <*0 *> is_a_proper_prefix_of x' ) ; :: thesis: b₁ in Z

hence x in Z by A4, A5, TARSKI:def 2, TREES_1:88; :: thesis: verum

end;

suppose ex s being FinSequence of NAT st
( s in Z | z & x' = <*0 *> ^ s ) ; :: thesis: b₁ in Z

hence x in Z by A3, TREES_1:def 9; :: thesis: verum

end;

end;

end;

hence Z = (elementary_tree 1) with-replacement <*0 *>,(Z | z) by TARSKI:2; :: thesis: verum