let T1, T2 be Tree; :: thesis: 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; :: thesis: ( ( 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) ) :: thesis: ( ( not p in T1 implies (T1 \/ T2) | p = T2 | p ) & ( not p in T2 implies (T1 \/ T2) | p = T1 | p ) )

proof

assume that
A1: p in T1 and
A2: p in T2 ; :: thesis: (T1 \/ T2) | p = (T1 | p) \/ (T2 | p)
let q be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not q in (T1 \/ T2) | p or q in (T1 | p) \/ (T2 | p) ) & ( not q in (T1 | p) \/ (T2 | p) or q in (T1 \/ T2) | p ) )
thus ( q in (T1 \/ T2) | p implies q in (T1 | p) \/ (T2 | p) ) :: thesis: ( not q in (T1 | p) \/ (T2 | p) or q in (T1 \/ T2) | p )

proof

assume q in (T1 \/ T2) | p ; :: thesis: q in (T1 | p) \/ (T2 | p)
then p ^ q in T1 \/ T2 by TREES_1:def 9;
then ( p ^ q in T1 or p ^ q in T2 ) by XBOOLE_0:def 3;
then ( q in T1 | p or q in T2 | p ) by A1, A2, TREES_1:def 9;
hence q in (T1 | p) \/ (T2 | p) by XBOOLE_0:def 3; :: thesis: verum

end;

assume q in (T1 | p) \/ (T2 | p) ; :: thesis: q in (T1 \/ T2) | p
then ( q in T1 | p or q in T2 | p ) by XBOOLE_0:def 3;
then ( p ^ q in T1 or p ^ q in T2 ) by A1, A2, TREES_1:def 9;
then p ^ q in T1 \/ T2 by XBOOLE_0:def 3;
hence q in (T1 \/ T2) | p by TREES_1:def 9; :: thesis: verum

end;

for T1, T2 being Tree
for p being Element of T1 \/ T2 st not p in T1 holds
(T1 \/ T2) | p = T2 | p

proof

let T1, T2 be Tree; :: thesis: for p being Element of T1 \/ T2 st not p in T1 holds
(T1 \/ T2) | p = T2 | p
let p be Element of T1 \/ T2; :: thesis: ( not p in T1 implies (T1 \/ T2) | p = T2 | p )
assume A3: not p in T1 ; :: thesis: (T1 \/ T2) | p = T2 | p
then A4: p in T2 by XBOOLE_0:def 3;
let q be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not q in (T1 \/ T2) | p or q in T2 | p ) & ( not q in T2 | p or q in (T1 \/ T2) | p ) )
thus ( q in (T1 \/ T2) | p implies q in T2 | p ) :: thesis: ( not q in T2 | p or q in (T1 \/ T2) | p )

proof

assume q in (T1 \/ T2) | p ; :: thesis: q in T2 | p
then p ^ q in T1 \/ T2 by TREES_1:def 9;
then ( p ^ q in T1 or p ^ q in T2 ) by XBOOLE_0:def 3;
hence q in T2 | p by A3, A4, TREES_1:46, TREES_1:def 9; :: thesis: verum

end;

assume q in T2 | p ; :: thesis: q in (T1 \/ T2) | p
then p ^ q in T2 by A4, TREES_1:def 9;
then p ^ q in T1 \/ T2 by XBOOLE_0:def 3;
hence q in (T1 \/ T2) | p by TREES_1:def 9; :: thesis: verum

end;

hence ( ( not p in T1 implies (T1 \/ T2) | p = T2 | p ) & ( not p in T2 implies (T1 \/ T2) | p = T1 | p ) ) ; :: thesis: verum