set e = elementary_tree 2;
let Z be Tree; :: thesis: for x1, x2 being Element of Z st x1 = <*0 *> & x2 = <*1*> & succ (Root Z) = {x1,x2} holds
Z = ((elementary_tree 2) with-replacement <*0 *>,(Z | x1)) with-replacement <*1*>,(Z | x2)
let x1, x2 be Element of Z; :: thesis: ( x1 = <*0 *> & x2 = <*1*> & succ (Root Z) = {x1,x2} implies Z = ((elementary_tree 2) with-replacement <*0 *>,(Z | x1)) with-replacement <*1*>,(Z | x2) )
assume that
A1: x1 = <*0 *> and
A2: x2 = <*1*> and
A3: succ (Root Z) = {x1,x2} ; :: thesis: Z = ((elementary_tree 2) with-replacement <*0 *>,(Z | x1)) with-replacement <*1*>,(Z | x2)
set T1 = (elementary_tree 2) with-replacement <*0 *>,(Z | x1);
A4: <*0 *> in elementary_tree 2 by ENUMSET1:def 1, TREES_1:90;

A5: now

let s be FinSequence of NAT ; :: thesis: ( ( not s in Z or ( s in (elementary_tree 2) with-replacement <*0 *>,(Z | x1) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) & ( ( ( s in (elementary_tree 2) with-replacement <*0 *>,(Z | x1) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) implies s in Z ) )
thus ( not s in Z or ( s in (elementary_tree 2) with-replacement <*0 *>,(Z | x1) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) :: thesis: ( ( ( s in (elementary_tree 2) with-replacement <*0 *>,(Z | x1) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) implies s in Z )

proof

assume A6: s in Z ; :: thesis: ( ( s in (elementary_tree 2) with-replacement <*0 *>,(Z | x1) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) )

per cases ( s = {} or s <> {} ) ;

suppose s = {} ; :: thesis: ( ( s in (elementary_tree 2) with-replacement <*0 *>,(Z | x1) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) )

hence ( ( s in (elementary_tree 2) with-replacement <*0 *>,(Z | x1) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) by TREES_1:36, TREES_1:39, TREES_1:47; :: thesis: verum

end;

suppose s <> {} ; :: thesis: ( ( s in (elementary_tree 2) with-replacement <*0 *>,(Z | x1) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) )

then consider w being FinSequence of NAT , n being Nat such that
A7: s = <*n*> ^ w by FINSEQ_2:150;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
<*n*> is_a_prefix_of s by A7, TREES_1:8;
then A8: <*n*> in Z by A6, TREES_1:45;
<*n*> = (Root Z) ^ <*n*> by FINSEQ_1:47;
then A9: <*n*> in succ (Root Z) by A8, TREES_2:14;

now

per cases ( <*n*> = <*0 *> or <*n*> = <*1*> ) by A1, A2, A3, A9, TARSKI:def 2;

suppose A10: <*n*> = <*0 *> ; :: thesis: ( ( s in (elementary_tree 2) with-replacement <*0 *>,(Z | x1) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) )

then w in Z | x1 by A1, A6, A7, TREES_1:def 9;
hence ( ( s in (elementary_tree 2) with-replacement <*0 *>,(Z | x1) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) by A4, A7, A10, Th5, TREES_1:def 12; :: thesis: verum

end;

suppose A11: <*n*> = <*1*> ; :: thesis: ( ( s in (elementary_tree 2) with-replacement <*0 *>,(Z | x1) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) )

then w in Z | x2 by A2, A6, A7, TREES_1:def 9;
hence ( ( s in (elementary_tree 2) with-replacement <*0 *>,(Z | x1) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) by A7, A11; :: thesis: verum

end;

end;

end;

hence ( ( s in (elementary_tree 2) with-replacement <*0 *>,(Z | x1) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) ; :: thesis: verum

end;

end;

end;

assume A12: ( ( s in (elementary_tree 2) with-replacement <*0 *>,(Z | x1) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) ; :: thesis: s in Z

now

per cases ( ( s in (elementary_tree 2) with-replacement <*0 *>,(Z | x1) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) by A12;

suppose A13: ( s in (elementary_tree 2) with-replacement <*0 *>,(Z | x1) & not <*1*> is_a_proper_prefix_of s ) ; :: thesis: s in Z

now

per cases ( ( s in elementary_tree 2 & not <*0 *> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x1 & s = <*0 *> ^ w ) ) by A4, A13, TREES_1:def 12;

suppose ( s in elementary_tree 2 & not <*0 *> is_a_proper_prefix_of s ) ; :: thesis: s in Z

then ( s = {} or s = <*0 *> or s = <*1*> ) by ENUMSET1:def 1, TREES_1:90;
hence s in Z by A1, A2, A3; :: thesis: verum

end;

suppose ex w being FinSequence of NAT st
( w in Z | x1 & s = <*0 *> ^ w ) ; :: thesis: s in Z

hence s in Z by A1, TREES_1:def 9; :: thesis: verum

end;

end;

end;

hence s in Z ; :: thesis: verum

end;

suppose ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ; :: thesis: s in Z

hence s in Z by A2, TREES_1:def 9; :: thesis: verum

end;

end;

end;

hence s in Z ; :: thesis: verum

end;

A14: now

assume <*0 *> is_a_proper_prefix_of <*1*> ; :: thesis: contradiction
then <*0 *> is_a_prefix_of <*1*> by XBOOLE_0:def 8;
hence contradiction by TREES_1:16; :: thesis: verum

end;

<*1*> in elementary_tree 2 by ENUMSET1:def 1, TREES_1:90;
then <*1*> in (elementary_tree 2) with-replacement <*0 *>,(Z | x1) by A4, A14, TREES_1:def 12;
hence Z = ((elementary_tree 2) with-replacement <*0 *>,(Z | x1)) with-replacement <*1*>,(Z | x2) by A5, TREES_1:def 12; :: thesis: verum