for Z, Z1, Z2 being Tree
for z being Element of Z st Z with-replacement (z,Z1) = Z with-replacement (z,Z2) holds
Z1 = Z2