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);

assume A6: t = <*1*> ^ p ; :: thesis: ( t in Leaves (tree (T0,T1)) iff p in Leaves 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

( ( 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 T1; :: thesis: ( t = <*1*> ^ p implies ( t in Leaves (tree (T0,T1)) iff p in Leaves T1 ) )( 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)) ) )

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;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 A4:
p in Leaves T0
; :: thesis: 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 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

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

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 A9:
p in Leaves T1
; :: thesis: 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 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

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