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 A1: ( p in W & q in W & 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
then ( not p is_a_prefix_of q & not q is_a_prefix_of p & not q,p are_c=-comparable ) by XBOOLE_0:def 9;
then A2: ( p in W with-replacement q,W2 & q in W with-replacement p,W1 ) by A1, 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 A2, 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 A1, Th2, TREES_1:def 12;
hence r in (W with-replacement q,W2) with-replacement p,W1 by A2, 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 A2, 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 A1, 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, Th2, TREES_1:def 12;
hence r in (W with-replacement p,W1) with-replacement q,W2 by A2, TREES_1:def 12; :: thesis: verum