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, XBOOLE_0:def 9;
not q is_a_prefix_of p by A3, XBOOLE_0:def 9;
then A6: p in W with-replacement q,W2 by A1, A2, Th9;
A7: q in W with-replacement p,W1 by A1, A2, A4, Th9;
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 A7, TREES_1:def 12;
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:8, TREES_1:def 12;
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 12;
hence r in (W with-replacement q,W2) with-replacement p,W1 by A6, TREES_1:def 12; :: 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 A6, TREES_1:def 12;
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:8, TREES_1:def 12;
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 12;
hence r in (W with-replacement p,W1) with-replacement q,W2 by A7, TREES_1:def 12; :: thesis: verum