let T1, T2 be Tree; :: thesis: tree T1,T2 = ((elementary_tree 2) with-replacement <*0 *>,T1) with-replacement <*1*>,T2
let p be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not p in tree T1,T2 or p in ((elementary_tree 2) with-replacement <*0 *>,T1) with-replacement <*1*>,T2 ) & ( not p in ((elementary_tree 2) with-replacement <*0 *>,T1) with-replacement <*1*>,T2 or p in tree T1,T2 ) )
A1: ( <*T1,T2*> . 1 = T1 & <*T1,T2*> . 2 = T2 & len <*T1,T2*> = 2 & 1 + 1 = 2 & 0 + 1 = 1 & {} in T1 & {} in T2 & 0 < 2 & 1 < 2 & 0 <> 1 ) by FINSEQ_1:61, TREES_1:47;
A2: ( <*0 *> in elementary_tree 2 & <*1*> in elementary_tree 2 & not <*0 *> is_a_proper_prefix_of <*1*> & not <*0 *> is_a_proper_prefix_of <*0 *> ) by ENUMSET1:def 1, TREES_1:89, TREES_1:90;
then A3: ( <*1*> in (elementary_tree 2) with-replacement <*0 *>,T1 & <*0 *> in (elementary_tree 2) with-replacement <*0 *>,T1 ) by TREES_1:def 12;
thus ( p in tree T1,T2 implies p in ((elementary_tree 2) with-replacement <*0 *>,T1) with-replacement <*1*>,T2 ) :: thesis: ( not p in ((elementary_tree 2) with-replacement <*0 *>,T1) with-replacement <*1*>,T2 or p in tree T1,T2 )

proof

assume A4: p in tree T1,T2 ; :: thesis: p in ((elementary_tree 2) with-replacement <*0 *>,T1) with-replacement <*1*>,T2

now

assume p <> {} ; :: thesis: p in ((elementary_tree 2) with-replacement <*0 *>,T1) with-replacement <*1*>,T2
then consider n being Element of NAT , q being FinSequence such that
A5: ( n < len <*T1,T2*> & q in <*T1,T2*> . (n + 1) & p = <*n*> ^ q ) by A4, Def15;
reconsider q = q as FinSequence of NAT by A5, FINSEQ_1:50;
A6: not <*1*> is_a_prefix_of <*0 *> ^ q by TREES_1:87;

A7: now

assume n = 0 ; :: thesis: p in ((elementary_tree 2) with-replacement <*0 *>,T1) with-replacement <*1*>,T2
then ( not <*1*> is_a_proper_prefix_of <*n*> ^ q & <*n*> ^ q in (elementary_tree 2) with-replacement <*0 *>,T1 ) by A1, A2, A5, A6, TREES_1:def 12, XBOOLE_0:def 8;
hence p in ((elementary_tree 2) with-replacement <*0 *>,T1) with-replacement <*1*>,T2 by A3, A5, TREES_1:def 12; :: thesis: verum

end;

n <= 0 + 1 by A1, A5, NAT_1:13;
then ( ( n = 1 & ( n = 1 implies <*n*> ^ q in ((elementary_tree 2) with-replacement <*0 *>,T1) with-replacement <*1*>,T2 ) ) or ( n >= 0 & n <= 0 ) ) by A1, A3, A5, NAT_1:8, TREES_1:def 12;
hence p in ((elementary_tree 2) with-replacement <*0 *>,T1) with-replacement <*1*>,T2 by A5, A7; :: thesis: verum

end;

hence p in ((elementary_tree 2) with-replacement <*0 *>,T1) with-replacement <*1*>,T2 by TREES_1:47; :: thesis: verum

end;

assume p in ((elementary_tree 2) with-replacement <*0 *>,T1) with-replacement <*1*>,T2 ; :: thesis: p in tree T1,T2
then A8: ( ( p in (elementary_tree 2) with-replacement <*0 *>,T1 & not <*1*> is_a_proper_prefix_of p ) or ex r being FinSequence of NAT st
( r in T2 & p = <*1*> ^ r ) ) by A3, TREES_1:def 12;

now

assume p in (elementary_tree 2) with-replacement <*0 *>,T1 ; :: thesis: p in tree T1,T2
then A9: ( ( p in elementary_tree 2 & not <*0 *> is_a_proper_prefix_of p ) or ex r being FinSequence of NAT st
( r in T1 & p = <*0 *> ^ r ) ) by A2, TREES_1:def 12;

now

assume p in elementary_tree 2 ; :: thesis: p in tree T1,T2
then ( ( p = {} or p = <*0 *> or p = <*1*> ) & p ^ {} = p ) by ENUMSET1:def 1, FINSEQ_1:47, TREES_1:90;
hence p in tree T1,T2 by A1, Def15; :: thesis: verum

end;

hence p in tree T1,T2 by A1, A9, Def15; :: thesis: verum

end;

hence p in tree T1,T2 by A1, A8, Def15; :: thesis: verum