let W, W1, W2 be Tree; 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 ; ( 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
; (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 ; TREES_2:def 1 ( 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) )
( 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)
;
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;
verum
end;
assume
r in (W with-replacement (q,W2)) with-replacement (p,W1)
; 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; verum