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 Nat such that
A3: p ^ <*n*> in T0 by TREES_1:55;
<*0*> ^ (p ^ <*n*>) in tree (T0,T1) by A3, TREES_3:69;
then (<*0*> ^ p) ^ <*n*> in tree (T0,T1) by FINSEQ_1:32;
hence contradiction by A1, A2, TREES_1:55; :: 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 Nat such that
A5: t ^ <*n*> in tree (T0,T1) by TREES_1:55;
<*0*> ^ (p ^ <*n*>) in tree (T0,T1) by A1, A5, FINSEQ_1:32;
then p ^ <*n*> in T0 by TREES_3:69;
hence contradiction by A4, TREES_1:55; :: 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 Nat such that
A8: p ^ <*n*> in T1 by TREES_1:55;
<*1*> ^ (p ^ <*n*>) in tree (T0,T1) by A8, TREES_3:70;
then (<*1*> ^ p) ^ <*n*> in tree (T0,T1) by FINSEQ_1:32;
hence contradiction by A6, A7, TREES_1:55; :: 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 Nat such that
A10: t ^ <*n*> in tree (T0,T1) by TREES_1:55;
<*1*> ^ (p ^ <*n*>) in tree (T0,T1) by A6, A10, FINSEQ_1:32;
then p ^ <*n*> in T1 by TREES_3:70;
hence contradiction by A9, TREES_1:55; :: thesis: verum