let T1, T2 be Tree; for p being Element of T1 \/ T2 holds
( ( p in T1 & p in T2 implies (T1 \/ T2) | p = (T1 | p) \/ (T2 | p) ) & ( not p in T1 implies (T1 \/ T2) | p = T2 | p ) & ( not p in T2 implies (T1 \/ T2) | p = T1 | p ) )
let p be Element of T1 \/ T2; ( ( p in T1 & p in T2 implies (T1 \/ T2) | p = (T1 | p) \/ (T2 | p) ) & ( not p in T1 implies (T1 \/ T2) | p = T2 | p ) & ( not p in T2 implies (T1 \/ T2) | p = T1 | p ) )
thus
( p in T1 & p in T2 implies (T1 \/ T2) | p = (T1 | p) \/ (T2 | p) )
( ( not p in T1 implies (T1 \/ T2) | p = T2 | p ) & ( not p in T2 implies (T1 \/ T2) | p = T1 | p ) )
for T1, T2 being Tree
for p being Element of T1 \/ T2 st not p in T1 holds
(T1 \/ T2) | p = T2 | p
hence
( ( not p in T1 implies (T1 \/ T2) | p = T2 | p ) & ( not p in T2 implies (T1 \/ T2) | p = T1 | p ) )
; verum