let T0, T1 be Tree; :: thesis: for t being Element of tree T0,T1 holds
( ( for p being Element of T0 st t = <*0 *> ^ p holds
( t in Leaves (tree T0,T1) iff p in Leaves T0 ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds
( t in Leaves (tree T0,T1) iff p in Leaves T1 ) ) )
let t be Element of tree T0,T1; :: thesis: ( ( for p being Element of T0 st t = <*0 *> ^ p holds
( t in Leaves (tree T0,T1) iff p in Leaves T0 ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds
( t in Leaves (tree T0,T1) iff p in Leaves T1 ) ) )
set RT = tree T0,T1;

hereby :: thesis: for p being Element of T1 st t = <*1*> ^ p holds
( t in Leaves (tree T0,T1) iff p in Leaves T1 )

let p be Element of T0; :: thesis: ( t = <*0 *> ^ p implies ( ( t in Leaves (tree T0,T1) implies p in Leaves T0 ) & ( p in Leaves T0 implies t in Leaves (tree T0,T1) ) ) )
assume A1: t = <*0 *> ^ p ; :: thesis: ( ( t in Leaves (tree T0,T1) implies p in Leaves T0 ) & ( p in Leaves T0 implies t in Leaves (tree T0,T1) ) )

hereby :: thesis: ( p in Leaves T0 implies t in Leaves (tree T0,T1) )

assume A2: t in Leaves (tree T0,T1) ; :: thesis: p in Leaves T0
assume not p in Leaves T0 ; :: thesis: contradiction
then consider n being Element of NAT such that
A3: p ^ <*n*> in T0 by TREES_1:92;
<*0 *> ^ (p ^ <*n*>) in tree T0,T1 by A3, TREES_3:72;
then (<*0 *> ^ p) ^ <*n*> in tree T0,T1 by FINSEQ_1:45;
hence contradiction by A1, A2, TREES_1:92; :: thesis: verum

end;

assume A4: p in Leaves T0 ; :: thesis: t in Leaves (tree T0,T1)
assume not t in Leaves (tree T0,T1) ; :: thesis: contradiction
then consider n being Element of NAT such that
A5: t ^ <*n*> in tree T0,T1 by TREES_1:92;
<*0 *> ^ (p ^ <*n*>) in tree T0,T1 by A1, A5, FINSEQ_1:45;
then p ^ <*n*> in T0 by TREES_3:72;
hence contradiction by A4, TREES_1:92; :: thesis: verum

end;

let p be Element of T1; :: thesis: ( t = <*1*> ^ p implies ( t in Leaves (tree T0,T1) iff p in Leaves T1 ) )
assume A6: t = <*1*> ^ p ; :: thesis: ( t in Leaves (tree T0,T1) iff p in Leaves T1 )

hereby :: thesis: ( p in Leaves T1 implies t in Leaves (tree T0,T1) )

assume A7: t in Leaves (tree T0,T1) ; :: thesis: p in Leaves T1
assume not p in Leaves T1 ; :: thesis: contradiction
then consider n being Element of NAT such that
A8: p ^ <*n*> in T1 by TREES_1:92;
<*1*> ^ (p ^ <*n*>) in tree T0,T1 by A8, TREES_3:73;
then (<*1*> ^ p) ^ <*n*> in tree T0,T1 by FINSEQ_1:45;
hence contradiction by A6, A7, TREES_1:92; :: thesis: verum

end;

assume A9: p in Leaves T1 ; :: thesis: t in Leaves (tree T0,T1)
assume not t in Leaves (tree T0,T1) ; :: thesis: contradiction
then consider n being Element of NAT such that
A10: t ^ <*n*> in tree T0,T1 by TREES_1:92;
<*1*> ^ (p ^ <*n*>) in tree T0,T1 by A6, A10, FINSEQ_1:45;
then p ^ <*n*> in T1 by TREES_3:73;
hence contradiction by A9, TREES_1:92; :: thesis: verum