let W, W1, W2 be Tree; :: thesis: for p, q being FinSequence of NAT st p in W & q in W & not p,q are_c=-comparable holds
(W with-replacement (p,W1)) with-replacement (q,W2) = (W with-replacement (q,W2)) with-replacement (p,W1)
let p, q be FinSequence of NAT ; :: thesis: ( p in W & q in W & not p,q are_c=-comparable implies (W with-replacement (p,W1)) with-replacement (q,W2) = (W with-replacement (q,W2)) with-replacement (p,W1) )
assume that
A1: p in W and
A2: q in W and
A3: not p,q are_c=-comparable ; :: thesis: (W with-replacement (p,W1)) with-replacement (q,W2) = (W with-replacement (q,W2)) with-replacement (p,W1)
A4: not p is_a_prefix_of q by A3;
not q is_a_prefix_of p by A3;
then A5: p in W with-replacement (q,W2) by A1, A2, Th7;
A6: q in W with-replacement (p,W1) by A1, A2, A4, Th7;
let r be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( r in (W with-replacement (p,W1)) with-replacement (q,W2) iff r in (W with-replacement (q,W2)) with-replacement (p,W1) )
thus ( r in (W with-replacement (p,W1)) with-replacement (q,W2) implies r in (W with-replacement (q,W2)) with-replacement (p,W1) ) :: thesis: ( r in (W with-replacement (q,W2)) with-replacement (p,W1) implies r in (W with-replacement (p,W1)) with-replacement (q,W2) )

proof

assume r in (W with-replacement (p,W1)) with-replacement (q,W2) ; :: thesis: r in (W with-replacement (q,W2)) with-replacement (p,W1)
then ( ( r in W with-replacement (p,W1) & not q is_a_proper_prefix_of r ) or ex r1 being FinSequence of NAT st
( r1 in W2 & r = q ^ r1 ) ) by A6, TREES_1:def 9;
then ( ( r in W & not p is_a_proper_prefix_of r & not q is_a_proper_prefix_of r ) or ( ex r2 being FinSequence of NAT st
( r2 in W1 & r = p ^ r2 ) & not q is_a_proper_prefix_of r ) or ( q is_a_prefix_of r & ex r1 being FinSequence of NAT st
( r1 in W2 & r = q ^ r1 ) ) ) by A1, TREES_1:1, TREES_1:def 9;
then ( ( r in W with-replacement (q,W2) & not p is_a_proper_prefix_of r ) or ex r1 being FinSequence of NAT st
( r1 in W1 & r = p ^ r1 ) ) by A2, A3, Th2, TREES_1:def 9;
hence r in (W with-replacement (q,W2)) with-replacement (p,W1) by A5, TREES_1:def 9; :: thesis: verum

end;

assume r in (W with-replacement (q,W2)) with-replacement (p,W1) ; :: thesis: r in (W with-replacement (p,W1)) with-replacement (q,W2)
then ( ( r in W with-replacement (q,W2) & not p is_a_proper_prefix_of r ) or ex r1 being FinSequence of NAT st
( r1 in W1 & r = p ^ r1 ) ) by A5, TREES_1:def 9;
then ( ( r in W & not q is_a_proper_prefix_of r & not p is_a_proper_prefix_of r ) or ( ex r2 being FinSequence of NAT st
( r2 in W2 & r = q ^ r2 ) & not p is_a_proper_prefix_of r ) or ( p is_a_prefix_of r & ex r1 being FinSequence of NAT st
( r1 in W1 & r = p ^ r1 ) ) ) by A2, TREES_1:1, TREES_1:def 9;
then ( ( r in W with-replacement (p,W1) & not q is_a_proper_prefix_of r ) or ex r1 being FinSequence of NAT st
( r1 in W2 & r = q ^ r1 ) ) by A1, A3, Th2, TREES_1:def 9;
hence r in (W with-replacement (p,W1)) with-replacement (q,W2) by A6, TREES_1:def 9; :: thesis: verum