for W, W1, W2 being 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)