for T being _Tree
for P being Path of T
for i, j being odd Nat st i < j & j <= len P holds
P . i <> P . j